Menkar: Towards a Multimode Presheaf Proof Assistant

Andreas Nuyts, Dominique Devriese

Research output: Unpublished contribution to conferenceUnpublished 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.
Original languageEnglish
Publication statusPublished - 13 Jun 2019
EventInternational Conference on Types for Proofs and Programs - Oslo, Norway
Duration: 11 Jun 201914 Jun 2019
Conference number: 25


ConferenceInternational Conference on Types for Proofs and Programs
Abbreviated titleTYPES
Internet address


  • Menkar
  • modal type theory

Cite this