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

Towards a computational interpretation of parametricity

Jean-Philippe Bernardy (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Guilhem Moulin (Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers))

Reynolds' abstraction theorem has recently been extended to lambda-calculi with dependent types. In this paper, we show how this theorem can be internalized. More precisely, we describe an extension of the Calculus of Constructions with a special parametricity rule (with computational content), and prove fundamental properties such as Church-Rosser's and strong normalization. The instances of the abstraction theorem can be both expressed and proved in the calculus itself.

Nyckelord: parametricity, type-theory, dependent types, lambda-calculi

Denna post skapades 2011-10-14. Senast ändrad 2012-01-16.
CPL Pubid: 147257