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

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))
IEEE Symposium on Logic in Computer Science. 27th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Dubrovnik, Croatia, June 25-28, 2012 (1043-6871). p. 135-144. (2012)
[Konferensbidrag, refereegranskat]

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 Pure Type Systems with a special parametricity rule (with computational content), and prove fundamental properties such as Church-Rosser's and strong normalization. All instances of the abstraction theorem can be both expressed and proved in the calculus itself. Moreover, one can apply parametricity to the parametricity rule: parametricity is itself parametric.

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

The link to Full Text gives the Extended Version.

Denna post skapades 2012-01-16. Senast ändrad 2012-11-09.
CPL Pubid: 153094


Läs direkt!

Lokal fulltext (fritt tillgänglig)

Länk till annan sajt (kan kräva inloggning)