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

Pure Type Systems with an Internalized Parametricity Theorem

Guilhem Moulin (Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers))
Göteborg : Chalmers University of Technology, 2013. - 82 s.

Parametricity results have recently been proved for dependently-typed calculi such as the Calculus of Constructions. However these results are meta theorems, and although they can be stated as internal propositions, they cannot be proved internally. In this thesis we define for any sufficiently strong Pure Type System O (such as the Calculus of Constructions) an extension P in which each instance of the parametricity theorem, including those corresponding to open terms, can be proved internally. As a consequence we can prove inside the system that each term of type forall A. A -> A is an identity. Furthermore, our system P is proved to be strongly normalizing by a reduction-preserving interpretation into O. We also prove Church-Rosser and Subject Reduction properties; consistency follows.

Nyckelord: Polymorphism, Parametricity, Type structure, Lambda Calculus.

Denna post skapades 2014-01-08. Senast ändrad 2016-04-15.
CPL Pubid: 191873


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, Datavetenskap, Programmeringslogik (Chalmers)


Teoretisk datalogi

Chalmers infrastruktur

Relaterade publikationer

Inkluderade delarbeten:

A Computational Interpretation of Parametricity


Datum: 2014-01-30
Tid: 10:00
Lokal: room HB2, Hörsalsvägen 8, Chalmers University of Technology
Opponent: Thorsten Altenkirch