Shallowly Embedding Type Theories as Presheaf Models in Agda: Extended Abstract

Onderzoeksoutput: Unpublished abstract

33 Downloads (Pure)

Samenvatting

We present work in progress on a shallow embedding of extensions of Martin-Löf Type Theory (MLTT) in Agda as presheaf models. In this way, a user wanting to explore some extension of MLTT can do so by instantiating our framework with a suitable base category, implementing the desired operations and axioms and then he/she can manipulate types and terms of the system in a similar way as in MLTT.
Originele taal-2English
Aantal pagina's3
StatusPublished - 23 aug 2020
EvenementWorkshop on Type-Driven Development - Online, Jersey City, United States
Duur: 23 aug 202023 aug 2020
https://icfp20.sigplan.org/home/tyde-2020

Workshop

WorkshopWorkshop on Type-Driven Development
Verkorte titelTyDe
LandUnited States
StadJersey City
Periode23/08/2023/08/20
Internet adres

Citeer dit