The following pages link to HOL (Q17631):
Displaying 50 items.
- Computer supported mathematics with \(\Omega\)MEGA (Q865650) (← links)
- SAD as a mathematical assistant -- how should we go from here to there? (Q865654) (← links)
- Providing a formal linkage between MDG and HOL (Q878110) (← links)
- A few exercises in theorem processing (Q879370) (← links)
- A complete axiom system for propositional projection temporal logic with cylinder computation model (Q896162) (← links)
- Formal probabilistic analysis of detection properties in wireless sensor networks (Q903510) (← links)
- A functional programming approach to the specification and verification of concurrent systems (Q909439) (← links)
- Refinement concepts formalised in higher order logic (Q916409) (← links)
- A mechanical analysis of program verification strategies (Q928673) (← links)
- A functional formalization of on chip communications (Q931433) (← links)
- The higher-order-logic Formath (Q935562) (← links)
- Proof synthesis and reflection for linear arithmetic (Q945055) (← links)
- The seven virtues of simple type theory (Q946569) (← links)
- Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms (Q964000) (← links)
- Partial and nested recursive function definitions in higher-order logic (Q972425) (← links)
- Interactive theorem proving. First international conference, ITP 2010, Edinburgh, UK, July 11--14, 2010. Proceedings (Q983522) (← links)
- Formalization of the standard uniform random variable (Q995466) (← links)
- HasCasl: integrated higher-order specification and program development (Q1006648) (← links)
- Adapting functional programs to higher order logic (Q1029815) (← links)
- Proof assistants: history, ideas and future (Q1040001) (← links)
- An extensible encoding of object-oriented data models in HOL. With an application to IMP++ (Q1040775) (← links)
- Data compression for proof replay (Q1040776) (← links)
- Using theorem proving to verify expectation and variance for discrete random variables (Q1040780) (← links)
- Verifying the unification algorithm in LCF (Q1060023) (← links)
- The notion of proof in hardware verification (Q1122998) (← links)
- Higher-order rewrite systems and their confluence (Q1127334) (← links)
- Theories for mechanical proofs of imperative programs (Q1267030) (← links)
- Formal verification of a programming logic for a distributed programming language (Q1285659) (← links)
- The \(HOL\) logic extended with quantification over type variables (Q1309243) (← links)
- Lazy techniques for fully expansive theorem proving (Q1309245) (← links)
- Mechanizing some advanced refinement concepts (Q1309250) (← links)
- A formal theory of simulations between infinite automata (Q1309253) (← links)
- An embedding of timed transition systems in \(HOL\) (Q1309256) (← links)
- Set theory for verification. I: From foundations to functions (Q1319386) (← links)
- IMPS: An interactive mathematical proof system (Q1319391) (← links)
- An exercise in the automatic verification of asynchronous designs (Q1329086) (← links)
- Constructing the real numbers in HOL (Q1334896) (← links)
- Modeling multi-rate DSP specification semantics for formal transformational design in HOL (Q1334899) (← links)
- Annotations in formal specifications and proofs (Q1334901) (← links)
- Verification of the Miller-Rabin probabilistic primality test. (Q1400288) (← links)
- A linear logical framework (Q1400718) (← links)
- A rewriting approach to satisfiability procedures. (Q1401930) (← links)
- Reuse of proofs in software verification (Q1419888) (← links)
- Algebraic models of correctness for abstract pipelines. (Q1426058) (← links)
- The calculus of constructions as a framework for proof search with set variable instantiation (Q1575927) (← links)
- Proof-search in type-theoretic languages: An introduction (Q1575935) (← links)
- Isabelle/HOL. A proof assistant for higher-order logic (Q1600086) (← links)
- Proof planning for strategy development (Q1601860) (← links)
- Making a productive use of failure to generate witnesses for coinduction from divergent proof attempts (Q1601863) (← links)
- Proof assistance for real-time systems using an interactive theorem prover (Q1603708) (← links)
