swMATH8360MaRDI QIDQ20369FDOQ20369
Author name not available (Why is that?)
Official website: http://www.cl.cam.ac.uk/~mjcg/papers/HolHistory.pdf
Cited In (only showing first 100 items - show all)
- Intuitionistic completeness of first-order logic
- Title not available (Why is that?)
- Automated proofs of object code for a widely used microprocessor
- A domain-theoretic model of nominally-typed object-oriented programming
- Notions of computation and monads
- Title not available (Why is that?)
- Eisbach: a proof method language for Isabelle
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
- LCF considered as a programming language
- Productive use of failure in inductive proof
- Repairing time-determinism in the process algebra for hybrid systems
- Efficiently checking propositional refutations in HOL theorem provers
- A logic covering undefinedness in program proofs
- The IO- and OI-hierarchies
- Embedding complex decision procedures inside an interactive theorem prover.
- ML
- Isar
- MetaPRL
- Miranda
- HOL
- Matita
- OCaml
- Nuprl
- Automath
- Isabelle/PIDE
- NQTHM
- ALF
- IMPS
- ValEncIA
- Bedwyr
- Minlog
- Squolem
- Milawa
- PhoX
- IsaFoR
- Analytica
- MDGs
- Jitawa
- Eisbach
- Mtac
- Camlp4
- Title not available (Why is that?)
- Preface to the special issue: Interactive theorem proving and the formalization of mathematics
- Challenges and experiences in managing large-scale proofs
- CLAM
- MKRP
- Elf
- SPEC
- Lucid
- ALGOL 60
- Horus
- Teyjus
- kepler98
- GETFOL
- Watson
- YACC
- ELPI
- Depth First Search
- MadMax
- Psyche
- MAGMA-Lisp
- Presburger Automata
- EVES
- Haskell Show Class
- Coccinelle
- Centaur
- Xml
- Omega-MKRP
- PRIZ
- XIsabelle
- Cambridge LCF
- Certification_Monads
- DefunT
- Groebner_Bases
- Group-Ring-Module
- Matrix_Tensor
- Jape
- OpenTheory
- TXDT
- Ruler
- TALx86
- Interactive theorem proving from the perspective of Isabelle/Isar
- Innovations in computational type theory using Nuprl
- Computational effects and operations: an overview
- Verification methods: rigorous results using floating-point arithmetic
- The Watson theorem prover
- A theory of type polymorphism in programming
- Analogy in inductive theorem proving
- OBSCURE, a specification language for abstract data types
- Partial and nested recursive function definitions in higher-order logic
- Termination of Isabelle functions via termination of rewriting
- Synthesis of ML programs in the system Coq
- Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture
- Title not available (Why is that?)
- A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
- Unification: A case-study in data refinement
- Flyspeck II: The basic linear programs
- A framework for developing stand-alone certifiers
- Type inference with recursive types: Syntax and semantics
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
This page was built for software: LCF
