CPL - Chalmers Publication Library

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

Författare och institution:
Jean-Philippe Bernardy (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Serie:
1) Doktorsavhandlingar vid Chalmers tekniska högskola. Ny serie, ISSN 0346-718X; nr 3195
2) Technical report D - Department of Computer Science and Engineering, Chalmers University of Technology and Göteborg University, ISSN 1653-1787; nr 77D
ISBN:
978-91-7385-514-3
Antal sidor:
135
Publikationstyp:
Doktorsavhandling
Förlag:
Chalmers University of Technology
Förlagsort:
Göteborg
Publiceringsår:
2011
Språk:
engelska
Datum för examination:
2011-06-07
Tidpunkt för examination:
10:00
Lokal:
lecture room EF, ED&IT building, Rännvägen 6B
Opponent:
Prof. Stephanie Weirich
Inkluderade delarbeten:
Fulltextlänk:
Sammanfattning (abstract):
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.
Ämne (baseras på Högskoleverkets indelning av forskningsämnen):
NATURVETENSKAP ->
Data- och informationsvetenskap ->
Datavetenskap (datalogi) ->
Teoretisk datalogi
NATURVETENSKAP ->
Data- och informationsvetenskap ->
Datavetenskap (datalogi) ->
Datalogi
Chalmers styrkeområden:
Informations- och kommunikationsteknik
Chalmers fundament:
Grundläggande vetenskaper
Postens nummer:
138141
Posten skapad:
2011-03-18 13:42
Posten ändrad:
2013-09-25 15:19

Visa i Endnote-format