Abstract
Andromeda is an LCFstyle proof assistant where the user builds derivable judgments by writing code in a metalevel programming language AML. The only trusted component of Andromeda is a minimalist nucleus (an implementation of the inference rules of an objectlevel type theory), which controls construction and decomposition of typetheoretic 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 metalanguage. 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 objectlevel 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 metatheoretic 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 lambdacalculus, and by implementing a simple automated system for managing a universe of types.
BibTeX  Entry
@InProceedings{bauer_et_al:LIPIcs:2018:9857,
author = {Andrej Bauer and Ga{\"e}tan Gilbert and Philipp G. Haselwarter and Matija Pretnar and Christopher A. Stone},
title = {{Design and Implementation of the Andromeda Proof Assistant}},
booktitle = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
pages = {5:15:31},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770651},
ISSN = {18688969},
year = {2018},
volume = {97},
editor = {Silvia Ghilezan and Herman Geuvers and Jelena Ivetić},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2018/9857},
URN = {urn:nbn:de:0030drops98574},
doi = {10.4230/LIPIcs.TYPES.2016.5},
annote = {Keywords: type theory, proof assistant, equality reflection, computational effects}
}
Keywords: 

type theory, proof assistant, equality reflection, computational effects 
Seminar: 

22nd International Conference on Types for Proofs and Programs (TYPES 2016) 
Issue Date: 

2018 
Date of publication: 

24.10.2018 