CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Towards Formalizing Categorical Models of Type Theory in Type Theory

Alexandre Buisse (Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers)) ; Peter Dybjer (Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers))
Electronic Notes in Theoretical Computer Science (1571-0661). Vol. 196 (2008), C, p. 137-151.
[Artikel, refereegranskad vetenskaplig]

This note is about work in progress on the topic of "internal type theory" where we investigate the internal formalization of the categorical metatheory of constructive type theory in (an extension of) itself. The basic notion is that of a category with families, a categorical notion of model of dependent type theory. We discuss how to formalize the notion of category with families inside type theory and how to build initial categories with families. Initial categories with families will be term models which play the role of canonical syntax for dependent type theory. We also discuss the formalization of the result that categories with finite limits give rise to categories with families. This yields a type-theoretic perspective on Curien's work on "substitution up to isomorphism". Our formalization is being carried out in the proof assistant Agda 2 developed at Chalmers.

Nyckelord: Categorical logic, categories with families, constructive type theory, dependent types, internal type theor , proof assistants



Denna post skapades 2015-02-11. Senast ändrad 2015-04-13.
CPL Pubid: 212424

 

Läs direkt!

Lokal fulltext (fritt tillgänglig)

Länk till annan sajt (kan kräva inloggning)