The following pages link to (Q4016540):
Displaying 18 items.
- On definitions of constants and types in HOL (Q287358) (← links)
- An extension of the Boyer-Moore theorem prover to support first-order quantification (Q688572) (← links)
- Rewriting with equivalence relations in ACL2 (Q928668) (← links)
- A mechanical analysis of program verification strategies (Q928673) (← links)
- Integrating external deduction tools with ACL2 (Q1006728) (← links)
- A verification system for concurrent programs based on the Boyer-Moore prover (Q1203115) (← links)
- Machine checked proofs of the design of a fault-tolerant circuit (Q1203129) (← links)
- A mechanically verified incremental garbage collector (Q1336946) (← links)
- Partial instantiation methods for inference in first-order logic (Q1610676) (← links)
- Milestones from the Pure Lisp Theorem Prover to ACL2 (Q2280212) (← links)
- Limited second-order functionality in a first-order setting (Q2303245) (← links)
- Specification and verification of concurrent programs through refinements (Q2351261) (← links)
- Theory extension in ACL2(r) (Q2642461) (← links)
- Second-Order Programs with Preconditions (Q3058455) (← links)
- An ACL2 Tutorial (Q3543644) (← links)
- First-order functional languages and intensional logic (Q4339019) (← links)
- A theorem prover for a computational logic (Q6488518) (← links)
- A macro for reusing abstract functions and theorems (Q6587251) (← links)
