Cambridge LCF
From MaRDI portal
Software:43692
swMATH31981MaRDI QIDQ43692FDOQ43692
Author name not available (Why is that?)
Source code repository: https://github.com/kohlhase/CambridgeLCF
Cited In (23)
- Codatatypes in ML
- Theo: An interactive proof development system
- A framework for developing stand-alone certifiers
- 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
- Reflection of formal tactics in a deductive reflection framework
- Experimenting with Isabelle in ZF set theory
- Computer assisted reasoning. A Festschrift for Michael J. C. Gordon
- Nuprl-Light: An implementation framework for higher-order logics
- A tactic language for refinement of state-rich concurrent specifications
- A logic for Miranda
- A fixedpoint approach to implementing (Co)inductive definitions
- 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
- The Strategy Challenge in SMT Solving
- 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
