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

A presheaf model of parametric type theory

Jean-Philippe Bernardy (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Thierry Coquand (Institutionen för data- och informationsteknik (GU) ; Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers)) ; Guilhem Moulin (Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers))
(2015)
[Preprint]

We propose a new type theory with internalized parametricity. Compared to previous similar proposals, this version comes with a denotational semantics which is a refinement of the standard presheaf semantics of dependent type theory. Further, this presheaf semantics is a refinement of the one used to interpret nominal sets with restrictions. The present calculus is a candidate for the core of a proof assistant with internalized parametricity.

Nyckelord: parametricity, presheaf semantics, type-theory



Denna post skapades 2015-02-16. Senast ändrad 2015-04-17.
CPL Pubid: 212680

 

Läs direkt!


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


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)
Institutionen för data- och informationsteknik (GU) (GU)
Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers)

Ämnesområden

Teoretisk datalogi

Chalmers infrastruktur