LCF
Edinburgh LCF. A mechanized logic of computation. From LCF to HOL: a short history. The original LCF system was a proof-checking program developed at Stanford University by Robin Milner in 1972. Descendents of LCF now form a thriving paradigm in computer assisted reasoning. Many of the developments of the last 25 years have been due to Robin Milner, whose in°uence on the ¯eld of automated reasoning has been diverse and profound. One of the descendents of LCF is HOL, a proof assistant for higher order logic originally developed for reasoning about hardware.2 The multi-faceted contribution of Robin Milner to the development of HOL is remarkable. Not only did he invent the LCF-approach to theorem proving, but he also designed the ML programming language underlying it and the innovative polymorphic type system used both by ML and the LCF and HOL logics. Code Milner wrote is still in use today, and the design of the hardware veri¯cation system LCF LSM (a now obsolete stepping stone from LCF to HOL) was inspired by Milner’s Calculus of Communicating Systems (CCS)
Keywords for this software
References in zbMATH (referenced in 157 articles , 1 standard article )
Showing results 1 to 20 of 157.
Sorted by year (- Lammich, Peter: Efficient verified (UN)SAT certificate checking (2020)
- Bentkamp, Alexander; Blanchette, Jasmin Christian; Klakow, Dietrich: A formal proof of the expressiveness of deep learning (2019)
- Miller, Dale: Mechanized metatheory revisited (2019)
- Moore, J. Strother: Milestones from the Pure Lisp Theorem Prover to ACL2 (2019)
- Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius: From LCF to Isabelle/HOL (2019)
- Matt, Christian; Maurer, Ueli; Portmann, Christopher; Renner, Renato; Tackmann, Björn: Toward an algebraic theory of systems (2018)
- Schlichtkrull, Anders: Formalization of the resolution calculus for first-order logic (2018)
- Chihani, Zakaria; Miller, Dale; Renaud, Fabien: A semantic framework for proof evidence (2017)
- Hales, Thomas; Adams, Mark; Bauer, Gertrud; Dang, Tat Dat; Harrison, John; Hoang Le Truong; Kaliszyk, Cezary; Magron, Victor; McLaughlin, Sean; Nguyen, Tat Thang; Nguyen, Quang Truong; Nipkow, Tobias; Obua, Steven; Pleso, Joseph; Rute, Jason; Solovyev, Alexey; Ta, Thi Hoai An; Tran, Nam Trung; Trieu, Thi Diep; Urban, Josef; Vu, Ky; Zumkeller, Roland: A formal proof of the Kepler conjecture (2017)
- Miller, Dale: Proof checking and logic programming (2017)
- Ziliani, Beta; Sozeau, Matthieu: A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading (2017)
- Adams, Mark: HOL zero’s solutions for Pollack-inconsistency (2016)
- Ayala-Rincón, Mauricio; Fernández, Maribel; Rocha-Oliveira, Ana Cristina: Completeness in PVS of a nominal unification algorithm (2016)
- Bettini, Lorenzo: Implementing type systems for the IDE with Xsemantics (2016)
- Calude, Cristian S.; Thompson, Declan: Incompleteness, undecidability and automated proofs (invited talk) (2016)
- Kumar, Ramana; Arthan, Rob; Myreen, Magnus O.; Owens, Scott: Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation (2016)
- Lin, Yuhui; Grov, Gudmund; Arthan, Rob: Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC (2016)
- Matichuk, Daniel; Murray, Toby; Wenzel, Makarius: Eisbach: a proof method language for Isabelle (2016)
- Sternagel, Christian; Thiemann, René: A framework for developing stand-alone certifiers (2015)
- Wenzel, Makarius: Interactive theorem proving from the perspective of Isabelle/Isar (2015)