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

zbMATH Keywords

type theorycomputational effectsproof assistantequality reflection

Mathematics Subject Classification ID

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

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)