The following pages link to LCF (Q20369):
Displaying 50 items.
- Synthesis of ML programs in the system Coq (Q1322847) (← links)
- OBSCURE, a specification language for abstract data types (Q1323328) (← links)
- Embedding complex decision procedures inside an interactive theorem prover. (Q1353946) (← links)
- Using tactics to reformulate formulae for resolution theorem proving (Q1380410) (← links)
- Program tactics and logic tactics (Q1380427) (← links)
- Proof planning for strategy development (Q1601860) (← links)
- Relative definability of boolean functions via hypergraphs (Q1605175) (← links)
- ELAN from a rewriting logic point of view (Q1608914) (← links)
- Formalization of the resolution calculus for first-order logic (Q1663242) (← links)
- A semantic framework for proof evidence (Q1701039) (← links)
- Completeness in PVS of a nominal unification algorithm (Q1744405) (← links)
- Toward an algebraic theory of systems (Q1786609) (← links)
- Writing programs that construct proofs (Q1820596) (← links)
- Towards a computation system based on set theory (Q1825191) (← links)
- Structuring metatheory on inductive definitions (Q1854368) (← links)
- Unification: A case-study in data refinement (Q1898815) (← links)
- Productive use of failure in inductive proof (Q1915134) (← links)
- An algorithm for type-checking dependent types (Q1916364) (← links)
- Formal verification of a partial-order reduction technique for model checking (Q1961915) (← links)
- Knowledge-based proof planning (Q1978469) (← links)
- Twee: an equational theorem prover (Q2055894) (← links)
- Guest editors' preface to special issue on interval temporal logics (Q2251123) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- Milestones from the Pure Lisp Theorem Prover to ACL2 (Q2280212) (← links)
- Mechanized metatheory revisited (Q2323447) (← links)
- Flyspeck II: The basic linear programs (Q2379683) (← links)
- Consistent and complementary formal theories of the semantics of programming languages (Q2561836) (← links)
- Proof checking and logic programming (Q2628296) (← links)
- Crystal: Integrating structured queries into a tactic language (Q2655333) (← links)
- A metatheory of a mechanized object theory (Q2676562) (← links)
- (Q2740996) (← links)
- (Q2767940) (← links)
- HOL Zero’s Solutions for Pollack-Inconsistency (Q2829240) (← links)
- Incompleteness, Undecidability and Automated Proofs (Q2829997) (← links)
- Practical Theory Extension in Event-B (Q2842627) (← links)
- (Q2844812) (← links)
- (Q2848688) (← links)
- (Q2851544) (← links)
- Psyche: A Proof-Search Engine Based on Sequent Calculus with an LCF-Style Architecture (Q2851941) (← links)
- Lightweight Static Capabilities (Q2866337) (← links)
- Verification methods: Rigorous results using floating-point arithmetic (Q2890535) (← links)
- Challenges and Experiences in Managing Large-Scale Proofs (Q2907311) (← links)
- Standalone Tactics Using OpenTheory (Q2914758) (← links)
- Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving (Q2986838) (← links)
- Realizability and Parametricity in Pure Type Systems (Q3000602) (← links)
- (Q3026376) (← links)
- Termination of Isabelle Functions via Termination of Rewriting (Q3088004) (← links)
- Validating QBF Validity in HOL4 (Q3088005) (← links)
- Proving Valid Quantified Boolean Formulas in HOL Light (Q3088006) (← links)
- Some Domain Theory and Denotational Semantics in Coq (Q3183523) (← links)