Write a Blog >>
ICFP 2020
Thu 20 - Fri 28 August 2020
Sun 23 Aug 2020 10:30 - 11:00 at TyDe - Session 1

We present work in progress on a shallow embedding of extensions of Martin-Löf Type Theory in Agda as presheaf models. More concretely, the terms, types, … of an object theory are represented in Agda using the presheaf construction and a user can manipulate them in the style of a category with families, with variables in de Bruijn form. Extra operations or axioms can be implemented by instantiating the framework with a suitable base category.

Extended Abstract (TyDeAbstract.pdf)343KiB

Sun 23 Aug
Times are displayed in time zone: Eastern Time (US & Canada) change

10:00 - 11:30: Session 1TyDe at TyDe
10:00 - 10:30
Practical Dependent Type Checking Using Twin Types
Víctor López JuanChalmers University of Technology, Nils Anders DanielssonUniversity of Gothenburg, Chalmers University of Technology
Media Attached
10:30 - 11:00
Shallowly Embedding Type Theories as Presheaf Models in Agda (Extended Abstract)
Joris CeulemansVrije Universiteit Brussel, Dominique DevrieseVrije Universiteit Brussel
File Attached
11:00 - 11:30
Generalization of Meta-Programs with Dependent Types in Mtac2 with Mtac2 (Extended Abstract)
Ignacio TiraboschiNone, Jan-Oliver KaiserMPI-SWS, Beta ZilianiFAMAF, UNC and CONICET