Menkar: Towards a Multimode Presheaf Proof Assistant

Andreas Nuyts, Dominique Devriese

Onderzoeksoutput: Unpublished paper


Recently, a number of extensions to dependent type theory have been proposed or refined that arenot easily added to pre-existing proof assistants as they severely impact the nature and manipu-lation of type-theoretic judgements and therefore require principled implementation choices fromthe start. For this reason, we have started the implementation in Haskell of a novel proof assistantMenkar1with the aim of supporting features that are relevant to studying modal and multimodetype theory as well as type-systems based on the internalization of properties of a presheaf model.We take a pragmatic approach, looking for a compromise between soundness, user-friendliness,ease of implementation, and flexibility with respect to foreseen and unforeseen modifications ofthe type system. Unlike projects such as NuPRL and Cedille, we do not intend to demonstrate analternative view on type theory. Instead, we keep Menkar very Agda-like and merely aim for animplementation of some recently proposed features. Below, we discuss how we (plan to) handleeach of the desired features. We conclude by listing possible applications.
Originele taal-2English
StatusPublished - 13 jun 2019
EvenementInternational Conference on Types for Proofs and Programs - Oslo, Norway
Duur: 11 jun 201914 jun 2019
Congresnummer: 25


ConferenceInternational Conference on Types for Proofs and Programs
Verkorte titelTYPES
Internet adres

Citeer dit