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

A Theory of Parametric Polymorphism and an Application

A formalisation of parametric polymorphism within and about dependent type-theory, and an application to property-based testing

Jean-Philippe Bernardy (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Göteborg : Chalmers University of Technology, 2011. ISBN: 978-91-7385-514-3.- 135 s.
[Doktorsavhandling]

This thesis revisits the well-known notion of parametric polymorphism in the light of modern developments in type-theory. Additionally, applications of parametric polymorphism are also presented. The first part of the thesis presents a theoretical investigation of the semantics of parametric polymorphism of and within type-theories with dependent types. It is shown how the meaning of polymorphic, possibly dependent, types can be reflected within type-theory itself, via a simple syntactic transformation. This self-referential property opens the door to internalise the transformation in type-theory, and we study one possible way to do so. We also examine how the translation relates to various specific features of type-theory, such as proof irrelevance and realizability. The second part is concerned an application of parametric polymorphism relevant to software engineers. We present a schema to reduce polymorphic properties to equivalent monomorphic properties, for the purpose of testing. Our proof uses parametricity and properties of initial algebras.



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

Läs mer om Chalmers styrkeområden  

Denna post skapades 2011-03-18. Senast ändrad 2013-09-25.
CPL Pubid: 138141