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

Realizability and Parametricity in Pure Type Systems

Jean-Philippe Bernardy (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Marc Lasson
Lecture Notes in Computer Science. 14th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2011 (0302-9743). Vol. 6604 (2011), p. 108-122.
[Konferensbidrag, refereegranskat]

We describe a systematic method to build a logic from any programming language described as a Pure Type System (PTS). The formulas of this logic express properties about programs. We define a parametricity theory about programs and a realizability theory for the logic. The logic is expressive enough to internalize both theories. Thanks to the PTS setting, we abstract most idiosyncrasies specific to particular type theories. This confers generality to the results, and reveals parallels between parametricity and realizability.

Nyckelord: parametricity realizability PTS



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

Läs mer om Chalmers styrkeområden  

Denna post skapades 2010-10-11. Senast ändrad 2012-02-15.
CPL Pubid: 127466

 

Läs direkt!

Lokal fulltext (fritt tillgänglig)

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