LCF swMATH ID: 8360 Software Authors: Milner, Robin Description: 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) Homepage: http://www.cl.cam.ac.uk/~mjcg/papers/HolHistory.pdf Related Software: ML; Coq; HOL; Nuprl; Isabelle; Isabelle/HOL; HOL Light; PVS; Automath; NQTHM; ACL2; Isar; Archive Formal Proofs; kepler98; Sledgehammer; z3; Mizar; seL4; Flyspeck; OCaml Cited in: 158 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year Edinburgh LCF. A mechanized logic of computation. Zbl 0421.68039Gordon, Michael J.; Milner, Arthur J.; Wadsworth, Christopher P. 1979 all top 5 Cited by 241 Authors 7 Constable, Robert Lee 5 Giunchiglia, Fausto 5 Huet, Gerard P. 5 Milner, Robin 4 Carlucci Aiello, Luigia 4 Plotkin, Gordon D. 4 Wenzel, Makarius 3 Aiello, Mario 3 Armando, Alessandro 3 Basin, David A. 3 Courcelle, Bruno 3 Kumar, Ramana 3 Melis, Erica 3 Nipkow, Tobias 3 Paulson, Lawrence Charles 3 Prini, Gianfranco 3 Traverso, Paolo 2 Adams, Mark 2 Arthan, Rob D. 2 Ashcroft, Edward A. 2 Attardi, Giuseppe 2 Berry, Gerard 2 Bickford, Mark 2 Blanchette, Jasmin Christian 2 Bundy, Alan 2 Coglio, Alessandro 2 Coppo, Mario 2 Coquand, Thierry 2 Egli, Herbert 2 Fernández, Maribel 2 Geuvers, Jan Herman 2 Gordon, Michael J. C. 2 Graham-Lengrand, Stéphane 2 Guessarian, Irène 2 Howe, Douglas J. 2 Ireland, Andrew 2 Kirchner, Claude 2 Kirchner, Hélène 2 Krauss, Alexander 2 Matthews, Seán 2 McLaughlin, Sean 2 Miller, Dale Allen 2 Moreau, Pierre-Etienne 2 Obua, Steven 2 Shankar, Natarajan 2 Sternagel, Christian 2 Thiemann, René 2 Vuillemin, Jean E. 2 Weber, Tjark 2 Weyhrauch, Richard W. 2 Whittle, Jon 1 AbdelGawad, Moez A. 1 Abramsky, Samson 1 Allen, Stuart F. 1 Alves-Foss, James 1 Amjad, Hasan 1 Asperti, Andrea 1 Ayala-Rincón, Mauricio 1 Barbanera, Franco 1 Barrett, Clark W. 1 Barringer, Howard 1 Bates, Joseph L. 1 Bauer, Andrej 1 Bauer, Gertrud 1 Beeson, Michael J. 1 Bentkamp, Alexander 1 Benton, Nick 1 Berghofer, Stefan 1 Bernardy, Jean-Philippe 1 Bettini, Lorenzo 1 Bidoit, Michel 1 Bird, Richard S. 1 Bonacina, Maria Paola 1 Bonnier, Staffan 1 Borovanský, Peter 1 Boulton, Richard J. 1 Bourke, Timothy 1 Boyer, Robert S. 1 Bucciarelli, Antonio 1 Calude, Cristian S. 1 Cardone, Felice 1 Cartwright, Robert 1 Cavallari, P. 1 Chihani, Zakaria 1 Chisholm, Paul 1 Chou, Ching-Tsun 1 Cirstea, Horatiu 1 Clarke, Edmund Melson jun. 1 Cohn, Avra 1 Cosserat, Laurent 1 Cuijpers, Pieter J. L. 1 Curien, Pierre-Louis 1 Daeche, N. 1 Damm, Werner 1 Dang, Tat Dat 1 Daum, Matthias 1 de Moura, Leonardo 1 Delahaye, David 1 Deville, Yves 1 Dietrich, Dominik ...and 141 more Authors all top 5 Cited in 35 Serials 19 Journal of Automated Reasoning 18 Theoretical Computer Science 6 Annals of Mathematics and Artificial Intelligence 5 Journal of Functional Programming 4 Acta Informatica 4 Journal of Computer and System Sciences 4 Formal Aspects of Computing 3 Science of Computer Programming 3 Journal of Symbolic Computation 3 Information and Computation 2 Artificial Intelligence 2 Information Processing Letters 2 SIAM Journal on Computing 2 Higher-Order and Symbolic Computation 2 Journal of Applied Logic 2 Lecture Notes in Computer Science 1 Letters in Mathematical Physics 1 Annales Scientifiques de l’Université de Clermont-Ferrand II. Mathématiques 1 Information and Control 1 ACM Transactions on Programming Languages and Systems 1 Annals of Pure and Applied Logic 1 MSCS. Mathematical Structures in Computer Science 1 Communications of the ACM 1 RAIRO. Informatique Théorique et Applications 1 Indagationes Mathematicae. New Series 1 Formal Methods in System Design 1 Journal of the ACM 1 LMS Journal of Computation and Mathematics 1 The Journal of Logic and Algebraic Programming 1 Sādhanā 1 Acta Numerica 1 Machine Intelligence 1 Journal of Formalized Reasoning 1 Forum of Mathematics, Pi 1 Journal of Logical and Algebraic Methods in Programming all top 5 Cited in 11 Fields 153 Computer science (68-XX) 54 Mathematical logic and foundations (03-XX) 5 Category theory; homological algebra (18-XX) 3 Order, lattices, ordered algebraic structures (06-XX) 2 General and overarching topics; collections (00-XX) 2 Systems theory; control (93-XX) 1 History and biography (01-XX) 1 Convex and discrete geometry (52-XX) 1 Numerical analysis (65-XX) 1 Operations research, mathematical programming (90-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year