Cited in
(42)- Codatatypes in ML
- Theo: An interactive proof development system
- A framework for developing stand-alone certifiers
- A fixedpoint approach to implementing (co)inductive definitions
- A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
- The foundation of a generic theorem prover
- Formal verification of a programming logic for a distributed programming language
- A framework for defining logical frameworks
- A fully automatic theorem prover with human-style output
- The strategy challenge in SMT solving
- Reflection of formal tactics in a deductive reflection framework
- Experimenting with Isabelle in ZF set theory
- Prosper
- Miranda
- ArcAngelC
- Nuprl
- NQTHM
- LCF
- LEGO
- GUARDIAN
- Elf
- SKIL
- GETFOL
- RDL
- AFFIRM
- Haskell Show Class
- Xml
- Tecton
- Certification_Monads
- Nuprl-Light
- Logipedia
- Computer assisted reasoning. A Festschrift for Michael J. C. Gordon
- A tactic language for refinement of state-rich concurrent specifications
- Nuprl-Light: An implementation framework for higher-order logics
- A logic for Miranda
- A reconstruction and extension of Maple's assume facility via constraint contextual rewriting
- An overview of the Tecton proof system
- Structured theory presentations and logic representations
- Proof-search in type-theoretic languages: An introduction
- Program tactics and logic tactics
- A logic for Miranda, revisited
- A higher-order calculus and theory abstraction
This page was built for software: Cambridge LCF
