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

Parametricity and dependent types

Jean-Philippe Bernardy (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Patrik Jansson (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Ross Paterson
International Conference on Functional Programming, September 27-29, 2010, Baltimore, Maryland (2010)
[Konferensbidrag, refereegranskat]

Reynolds' abstraction theorem shows how a typing judgement in System F can be translated into a relational statement (in second order predicate logic) about inhabitants of the type. We expose a similar result, where terms, types, and their relations are expressed in a single typed lambda calculus (a pure type system). Working within a single system dispenses the need for an interpretation layer, allowing for an unusually simple presentation. While the unification puts some constraints on the type system (which we spell out), the result applies to many interesting cases, including dependently-typed ones.

Nyckelord: Parametricity, Dependent types, Pure type systems



Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2010-03-31. Senast ändrad 2014-09-02.
CPL Pubid: 118913

 

Läs direkt!

Lokal fulltext (fritt tillgänglig)


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers) (2008-2010)

Ämnesområden

Informations- och kommunikationsteknik
Teoretisk datalogi
Datalogi

Chalmers infrastruktur

Relaterade publikationer

Denna publikation ingår i:


A Theory of Parametric Polymorphism and an Application