LEGO
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.
Keywords for this software
References in zbMATH (referenced in 62 articles )
Showing results 1 to 20 of 62.
Sorted by year (- Charguéraud, Arthur: The locally nameless representation (2012)
- Felty, Amy; Momigliano, Alberto: Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (2012)
- Ranta, Aarne: Machine translation and type theory (2012)
- Dennis, Louise Abigail; Green, Ian; Smaill, Alan: The use of embeddings to provide a clean separation of term and annotation for higher order rippling (2011)
- Lengrand, Stéphane Jean Eric; Dyckhoff, Roy; McKinna, James: A focused sequent calculus framework for proof search in pure type systems (2011)
- Geuvers, H.: Proof assistants: history, ideas and future (2009)
- Luo, Zhaohui; Adams, Robin: Structural subtyping for inductive types with functorial equality rules (2008)
- Nanevski, Aleksandar; Morrisett, Greg; Shinnar, Avraham; Govereau, Paul; Birkedal, Lars: Ynot: dependent types for imperative programs (2008)
- Caldwell, James; Pohl, Josef: Constructive membership predicates as index types. (2007)
- Moczydłowski, Wojciech: A normalizing intuitionistic set theory with inaccessible sets (2007)
- Sheard, Tim: Type-level computation using narrowing in omegamega. (2007)
- Brady, Edwin; Hammond, Kevin: A dependently typed framework for static analysis of program execution costs (2006)
- Aydemir, Brian E.; Bohannon, Aaron; Fairbairn, Matthew; Foster, J.Nathan; Pierce, Benjamin C.; Sewell, Peter; Vytiniotis, Dimitrios; Washburn, Geoffrey; Weirich, Stephanie; Zdancewic, Steve: Mechanized metatheory for the masses: the PoplMark challenge (2005)
- Luo, Zhaohui; Luo, Yong: Transitivity in coercive subtyping (2005)
- McBride, Conor: Epigram: Practical programming with dependent types (2005)
- Verdejo, Alberto; Martí-Oliet, Narciso: Two case studies of semantics execution in Maude: CCS and LOTOS (2005)
- Westbrook, Edwin; Stump, Aaron; Wehrman, Ian: A language-based approach to functionally correct imperative programming (2005)
- Wiedijk, Freek (ed.): The seventeen provers of the world. Foreword by Dana S. Scott.. (2005)
- Bertot, Yves; Castéran, Pierre: Interactive theorem proving and program development. Coq’Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring. (2004)
- Brady, Edwin; McBride, Conor; McKinna, James: Inductive families need not store their indices (2004)
Further publications can be found at: http://www.dcs.ed.ac.uk/home/lego/html/papers.html