The following pages link to Cambridge LCF (Q43692):
Displaying 24 items.
- (Q47686) (redirect page) (← links)
- A framework for developing stand-alone certifiers (Q530847) (← links)
- A tactic language for refinement of state-rich concurrent specifications (Q541214) (← links)
- Theo: An interactive proof development system (Q688727) (← links)
- Codatatypes in ML (Q908682) (← links)
- A logic for Miranda (Q909443) (← links)
- A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction (Q1075050) (← links)
- Formal verification of a programming logic for a distributed programming language (Q1285659) (← links)
- Experimenting with Isabelle in ZF set theory (Q1312157) (← links)
- Structured theory presentations and logic representations (Q1326777) (← links)
- An overview of the Tecton proof system (Q1341710) (← links)
- Program tactics and logic tactics (Q1380427) (← links)
- Proof-search in type-theoretic languages: An introduction (Q1575935) (← links)
- The foundation of a generic theorem prover (Q1823013) (← links)
- A logic for Miranda, revisited (Q1903076) (← links)
- A fully automatic theorem prover with human-style output (Q2362206) (← links)
- A reconstruction and extension of Maple's assume facility via constraint contextual rewriting (Q2456557) (← links)
- A higher-order calculus and theory abstraction (Q2639838) (← links)
- Computer assisted reasoning. A Festschrift for Michael J. C. Gordon (Q2655321) (← links)
- A Framework for Defining Logical Frameworks (Q2864157) (← links)
- Reflection of formal tactics in a deductive reflection framework (Q4647552) (← links)
- The Strategy Challenge in SMT Solving (Q4913859) (← links)
- A fixedpoint approach to implementing (Co)inductive definitions (Q5210768) (← links)
- Nuprl-Light: An implementation framework for higher-order logics (Q5234721) (← links)
