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 ; Guilhem Moulin (Institutionen för data- och informationsteknik, Datavetenskap (Chalmers))
Electronical Notes in Theoretical Computer Science (1571-0661). Vol. 319 (2015), p. 67-82.
[Artikel, refereegranskad vetenskaplig]

We extend Martin-Löf's Logical Framework with special constructions and typing rules providing 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 2016-01-15. Senast ändrad 2016-01-15.
CPL Pubid: 230735

 

Läs direkt!

Lokal fulltext (fritt tillgänglig)

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, datavetenskap, programmeringslogik (GU) (GU)
Institutionen för data- och informationsteknik, Datavetenskap (Chalmers)

Ämnesområden

Teoretisk datalogi

Chalmers infrastruktur

Relaterade publikationer

Denna publikation ingår i:


Internalizing Parametricity