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.
|Publication status||Published - 13 Jun 2019|
|Event||International Conference on Types for Proofs and Programs - Oslo, Norway|
Duration: 11 Jun 2019 → 14 Jun 2019
Conference number: 25
|Conference||International Conference on Types for Proofs and Programs|
|Period||11/06/19 → 14/06/19|
- modal type theory