Design and Implementation of the Andromeda Proof Assistant

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

Thumbnail PDF


  • Filesize: 0.61 MB
  • 31 pages

Document Identifiers

Author Details

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

Cite AsGet BibTex

Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter, Matija Pretnar, and Christopher A. Stone. Design and Implementation of the Andromeda Proof Assistant. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 5:1-5:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Andromeda is an LCF-style proof assistant where the user builds derivable judgments by writing code in a meta-level programming language AML. The only trusted component of Andromeda is a minimalist nucleus (an implementation of the inference rules of an object-level type theory), which controls construction and decomposition of type-theoretic judgments. Since the nucleus does not perform complex tasks like equality checking beyond syntactic equality, this responsibility is delegated to the user, who implements one or more equality checking procedures in the meta-language. The AML interpreter requests witnesses of equality from user code using the mechanism of algebraic operations and handlers. Dynamic checks in the nucleus guarantee that no invalid object-level derivations can be constructed. To demonstrate the flexibility of this system structure, we implemented a nucleus consisting of dependent type theory with equality reflection. Equality reflection provides a very high level of expressiveness, as it allows the user to add new judgmental equalities, but it also destroys desirable meta-theoretic properties of type theory (such as decidability and strong normalization). The power of effects and handlers in AML is demonstrated by a standard library that provides default algorithms for equality checking, computation of normal forms, and implicit argument filling. Users can extend these new algorithms by providing local "hints" or by completely replacing these algorithms for particular developments. We demonstrate the resulting system by showing how to axiomatize and compute with natural numbers, by axiomatizing the untyped lambda-calculus, and by implementing a simple automated system for managing a universe of types.
  • type theory
  • proof assistant
  • equality reflection
  • computational effects


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Andreas Abel and Jesper Cockx. Sprinkles of extensionality for your vanilla type theory. In 22nd International Conference on Types for Proofs and Programs, TYPES 2016, Novi Sad, Serbia, May 2016. Google Scholar
  2. S.F. Allen, M. Bickford, R.L. Constable, R. Eaton, C. Kreitz, L. Lorigo, and E. Moran. Innovations in computational type theory using Nuprl. Journal of Applied Logic, 4(4):428-469, 2006. Google Scholar
  3. Andrej Bauer and Matija Pretnar. Programming with algebraic effects and handlers. Journal of Logical and Algebraic Methods in Programming, 84(1):108-123, January 2015. Google Scholar
  4. William J. Bowman. Growing a proof assistant. In Higher-Order Programming with Effects, 2016. Google Scholar
  5. Paolo Capriotti. Notions of type formers. In 23rd International Conference on Types for Proofs and Programs (TYPES). Budapest, Hungary, May 29-June 1 2017. Google Scholar
  6. Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5(2):56-68, 1940. URL:
  7. Coq Development Team. The Coq proof assistant. Available at, 2016.
  8. Thierry Coquand. An Algorithm for Testing Conversion in Type Theory. In Gérard Huet and G. Plotkin, editors, Logical frameworks, pages 255-277. Cambridge University Press, 1991. Google Scholar
  9. Luis Damas and Robin Milner. Principal type-schemes for functional programs. In Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '82), pages 207-212, 1982. Google Scholar
  10. Leonardo de Moura, Soonho Kong, Floris van Doorn, Jakob von Raumer, and Jeremy Avigad. The Lean theorem prover (system description). In 25th International Conference on Automated Deduction (CADE-25), 2015. Google Scholar
  11. Jean-Yves Girard. Interprétation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur. PhD thesis, Université Paris VII, 1972. Google Scholar
  12. Michael J. Gordon, Arthur J. Milnter, and Christopher P. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation. Number 78 in Lecture Notes in Computer Science. Springer-Verlag, 1979. Google Scholar
  13. John Harrison. The HOL Light theorem prover. Available at URL:
  14. Martin Hofmann. Extensional constructs in intensional type theory. CPHC/BCS distinguished dissertations. Springer, 1997. Google Scholar
  15. HOL Interactive Theorem Prover. Available at URL:
  16. Isabelle proof assistant. Available at URL:
  17. Per Martin-Löf and Giovanni Sambin. Intuitionistic type theory. Studies in Proof Theory. Bibliopolis, 1984. Google Scholar
  18. Robin Milner, Mads Tofte, and Robert Harper. The Definition of Standard ML. MIT Press, 1990. Google Scholar
  19. Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology, 2007. Google Scholar
  20. OCaml programming language. Available at URL:
  21. Gordon D. Plotkin and Matija Pretnar. Handlers of algebraic effects. In Proceedings of the 18th European Symposium on Programming Languages and Systems, pages 80-94, 2009. Google Scholar
  22. Gordon D. Plotkin and Matija Pretnar. Handling algebraic effects. Logical Methods in Computer Science, 9(4), 2013. URL:
  23. Matija Pretnar. An introduction to algebraic effects and handlers. invited tutorial paper. Electronic Notes in Theoretical Computer Science, 319:19-35, 2015. URL:
  24. Christopher A. Stone and Robert Harper. Extensional equivalence and singleton types. ACM Transactions on Computational Logic, 7(4):676-722, October 2006. Google Scholar
  25. Thomas Streicher. Investigations into intensional type theory. Habilitation Thesis, Ludwig-Maximilians Universität, 1993. Google Scholar
  26. Coq Development Team. The Coq proof assistant reference manual, version 8.5. Available at URL:
  27. Beta Ziliani and Matthieu Sozeau. A Unification Algorithm for Coq featuring Universe Polymorphism and Overloading. In ACM SIGPLAN International Conference on Functional Programming 2015, 2015. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail