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

Internalizing Parametricity

Guilhem Moulin (Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers))
Göteborg : Chalmers University of Technology, 2016. ISBN: 978-91-7597-384-5.- 184 s.
[Doktorsavhandling]

Parametricity results have recently been proved for dependently-typed calculi such as the Calculus of Constructions. However these results are meta theorems, and although the theorems can be stated as internal propositions, they cannot be proved internally. In this thesis, we develop a dependent type-theory in which each instance of the parametricity theorem, including those for open terms, can be proved internally. For instance we can prove inside the system that each term of type (X : *) -> X -> X is an identity. We show three successive proposals for a solution to this problem, each an improvement of the previous one. In the first one we introduce a dependent type theory with special syntax for hypercubes. In the second proposal we outline a colored type theory, which provides a simplification of the type theory with hypercubes. In the third and final proposal, we give a more definite presentation of the colored type theory. We also prove its consistency by a modification of the presheaf model of dependent type theory. We believe that our final colored type theory is simple enough to provide a basis for a proof assistant where proofs relying on parametricity can be performed internally.

Nyckelord: Polymorphism, Parametricity, Type structure, Lambda Calculus, Presheaf Model



Denna post skapades 2016-05-02. Senast ändrad 2016-10-13.
CPL Pubid: 235758

 

Läs direkt!

Lokal fulltext (fritt tillgänglig)


Institutioner (Chalmers)

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

Ämnesområden

Teoretisk datalogi

Chalmers infrastruktur

Relaterade publikationer

Inkluderade delarbeten:


A Computational Interpretation of Parametricity


Type-Theory In Color


A Presheaf Model of Parametric Type Theory


Examination

Datum: 2016-05-30
Tid: 10:00
Lokal: EB
Opponent: Tarmo Uustalu

Ingår i serie

Doktorsavhandlingar vid Chalmers tekniska högskola. Ny serie 4065