LEGO swMATH ID: 9685 Software Authors: Luo, Z., Pollack, R. Description: LEGO is an interactive proof development system (proof assistant) designed and implemented by Randy Pollack in Edinburgh using New Jersey ML. It implements various related type systems - the Edinburgh Logical Framework (LF), the Calculus of Constructions (CC), the Generalized Calculus of Constructions (GCC) and the Unified Theory of Dependent Types (UTT). LEGO is a powerful tool for interactive proof development in the natural deduction style. It supports refinement proof as a basic operation. The system design emphasizes removing the more tedious aspects of interactive proofs. For example, features of the system like argument synthesis and universe polymorphism make proof checking more practical by bringing the level of formalization closer to that of informal mathematics. The higher-order power of its underlying type theories, and the support of specifying new inductive types, provide an expressive language for formalization of mathematical problems and program specification and development. Homepage: http://www.dcs.ed.ac.uk/home/lego/ Related Software: Coq; Nuprl; Automath; Isabelle; ML; HOL; PVS; Twelf; ALF; Isabelle/HOL; Plastic; Haskell; Cayenne; Cambridge LCF; Elf; Analytica; Epigram; PoplMark; Isar; NQTHM Cited in: 106 Publications Further Publications: http://www.dcs.ed.ac.uk/home/lego/html/papers.html all top 5 Cited by 134 Authors 8 Luo, Zhaohui 7 Barthe, Gilles 6 Pollack, Robert 5 Altenkirch, Thorsten 5 McBride, Conor Thomas 4 Honsell, Furio 4 Pfenning, Frank 3 Abel, Andreas M. 3 Brady, Edwin C. 3 McKinna, James 3 Miculan, Marino 3 Moczydłowski, Wojciech 3 Schürmann, Carsten 2 Barendregt, Hendrik Pieter 2 Buchberger, Bruno 2 Caldwell, James L. 2 Dybjer, Peter 2 Geuvers, Jan Herman 2 Hatcliff, John 2 Oostdijk, Martijn Diederik 2 Paulin-Mohring, Christine 2 Reus, Bernhard 2 Ricciotti, Wilmer 2 Solov’ëv, Sergeĭ Vladimirovich 2 Stump, Aaron 1 Aczel, Peter 1 Adams, Robin 1 Asperti, Andrea 1 Aspinall, David 1 Avron, Arnon 1 Aydemir, Brian E. 1 Barendsen, Erik 1 Berghofer, Stefan 1 Bertot, Yves 1 Birkedal, Lars 1 Blanqui, Frédéric 1 Bloo, Roel 1 Bohannon, Aaron 1 Bruni, Roberto 1 Cáccamo, Mario 1 Caprotti, Olga 1 Casteran, Pierre 1 Chapman, James T. E. 1 Charguéraud, Arthur 1 Cockx, Jesper 1 Cohen, Arjeh Marcel 1 Cormack, Gordon V. 1 Courtieu, Pierre 1 Crole, Roy L. 1 Damiani, Ferruccio 1 David, Rene 1 Delahaye, David 1 Denney, Ewen 1 Dennis, Louise Abigail 1 Devriese, Dominique 1 Dill, David L. 1 Duggan, Dominic 1 Dyckhoff, Roy 1 Fairbairn, Matthew W. 1 Farmer, William M. 1 Felty, Amy P. 1 Foster, J. Nathan 1 Galmiche, Didier 1 Gent, Ian Philip 1 Goubault-Larrecq, Jean 1 Govereau, Paul 1 Green, Ian 1 Hammond, Kevin 1 Harper, Robert 1 Hudak, Paul 1 Ireland, Andrew 1 Jones, Alex K. 1 Kamareddine, Fairouz D. 1 Kapur, Deepak 1 Kleymann, Thomas 1 Kutsia, Temur 1 Lengrand, Stéphane Jean Eric 1 Lenisa, Marina 1 Luo, Yong 1 Luther, Marko 1 Martí-Oliet, Narciso 1 Mason, Ian A. 1 Mayero, Micaela 1 Mendler, Michael 1 Momigliano, Alberto 1 Morris, Peter A. 1 Morrisett, Greg 1 Musser, David R. 1 Nanevski, Aleksandar 1 Nederpelt, Rob 1 Nipkow, Tobias 1 Ophel, John 1 Ore, Christian-Emil 1 Parent-Vigouroux, Catherine 1 Pierce, Benjamin C. 1 Piessens, Frank 1 Pohl, Josef 1 Pollack, Randy 1 Pons, Olivier 1 Prost, Frédéric ...and 34 more Authors all top 5 Cited in 19 Serials 11 Theoretical Computer Science 8 Journal of Automated Reasoning 4 Information and Computation 3 Annals of Pure and Applied Logic 3 Formal Aspects of Computing 3 MSCS. Mathematical Structures in Computer Science 2 Journal of Symbolic Computation 2 Sādhanā 2 Journal of Applied Logic 2 Logical Methods in Computer Science 1 Acta Informatica 1 Journal of Computer Science and Technology 1 Formal Methods in System Design 1 Journal of Functional Programming 1 Annals of Mathematics and Artificial Intelligence 1 RAIRO. Theoretical Informatics and Applications 1 International Series of Monographs on Computer Science 1 Lecture Notes in Computer Science 1 Texts in Theoretical Computer Science. An EATCS Series all top 5 Cited in 8 Fields 94 Computer science (68-XX) 58 Mathematical logic and foundations (03-XX) 4 Category theory; homological algebra (18-XX) 1 General and overarching topics; collections (00-XX) 1 History and biography (01-XX) 1 Group theory and generalizations (20-XX) 1 Information and communication theory, circuits (94-XX) 1 Mathematics education (97-XX) Citations by Year