Design and implementation of the andromeda proof assistant

DOI10.4230/LIPICS.TYPES.2016.5MaRDI QIDQ6855252zbMATH OpenFDO

Authors Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter, Matija Pretnar, Christopher A. Stone

Publication date 20 February 2026

Copyright license Creative Commons Attribution 3.0 Unported

Full work available at URL https://doi.org/10.4230/LIPICS.TYPES.2016.5

zbMATH Keywords

computational effectsequality reflectionproof assistanttype theory

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites work

• A formulation of the simple theory of types.
• A unification algorithm for Coq featuring universe polymorphism and overloading
• An introduction to algebraic effects and handlers (invited tutorial paper)
• Edinburgh LCF. A mechanized logic of computation
• Extensional constructs in intensional type theory
• Extensional equivalence and singleton types
• Handlers of Algebraic Effects
• Handling algebraic effects
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 65534 (Why is no real title available?)
• Innovations in computational type theory using Nuprl
• Programming with algebraic effects and handlers
• The Lean theorem prover (system description)

This page was built for publication: Design and implementation of the andromeda proof assistant

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6855252)