AESOP home

Publications

A projection model of types

David J Lillie, Peter G. Harrison

Conference or Workshop Paper
5th ACM conference on Functional programming languages and computer architecture
July, 1991
Lecture Notes in Computer Science
Volume 523
pp.259–288
Springer
DOI 10.1007/3540543961_13
Abstract

We present an intuitive model of polymorphic recursive types and subtypes based on a metric space of projections. We show this model to be semantically equivalent to types as strong ideals although requiring less structure in the semantic framework and allowing a more concise analysis. We present a new set of type inference rules for a combinatorial language and prove the rules correct with respect to our model. An algorithm embodying these rules has been implemented.

Information from pubs.doc.ic.ac.uk/projection-model-types.