LCF
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 110 articles )
Showing results 1 to 20 of 110.
Sorted by year (- Bettini, Lorenzo: Implementing type systems for the IDE with Xsemantics (2016)
- Kumar, Ramana; Arthan, Rob; Myreen, Magnus O.; Owens, Scott: Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation (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)
- AbdelGawad, Moez A.: A domain-theoretic model of nominally-typed object-oriented programming (2014)
- Constable, Robert; Bickford, Mark: Intuitionistic completeness of first-order logic (2014)
- Moszkowski, Ben (ed.); Guelev, Dimitar (ed.); Leucker, Martin (ed.): Guest editors’ preface to special issue on interval temporal logics (2014)
- Geuvers, Herman; Nederpelt, Rob: N. G. de Bruijn’s contribution to the formalization of mathematics (2013)
- Khadim, U.; Cuijpers, P.J.L.: Repairing time-determinism in the process algebra for hybrid systems (2012)
- Bernardy, Jean-Philippe; Lasson, Marc: Realizability and parametricity in pure type systems (2011)
- Asperti, Andrea; Sacerdoti Coen, Claudio: Some considerations on the usability of interactive provers (2010)
- Dietrich, Dominik; Schulz, Ewaryst: Crystal: Integrating structured queries into a tactic language (2010)
- Kirchner, Florent; Muñoz, César: The proof monad (2010)
- Platzer, Andé: Logical analysis of hybrid systems. Proving theorems for complex dynamics. (2010)
- Rump, Siegfried M.: Verification methods: rigorous results using floating-point arithmetic (2010)
- Abed, Sa’ed; Mohamed, Otmane Ait; Al-Sammane, Ghiath: An abstract reachability approach by combining HOL induction and multiway decision graphs (2009)
- Geuvers, H.: Proof assistants: history, ideas and future (2009)
- Obua, Steven; Nipkow, Tobias: Flyspeck II: The basic linear programs (2009)
- Weber, Tjark; Amjad, Hasan: Efficiently checking propositional refutations in HOL theorem provers (2009)
- Cirstea, Horatiu; Faure, Germain; Kirchner, Claude: A $\rho$-calculus of explicit constraint application (2007)