Show simple item record

dc.contributor.authorDonnelly, Kevinen_US
dc.date.accessioned2011-10-20T04:42:48Z
dc.date.available2011-10-20T04:42:48Z
dc.date.issued2007en_US
dc.identifier.urihttp://hdl.handle.net/2144/1692
dc.description.abstractSystem F is a type system that can be seen as both a proof system for second-order propositional logic and as a polymorphic programming language. In this work we explore several extensions of System F by types which express subtyping constraints. These systems include terms which represent proofs of subtyping relationships between types. Given a proof that one type is a subtype of another, one may use a coercion term constructor to coerce terms from the first type to the second. The ability to manipulate type constraints as first-class entities gives these systems a lot of expressive power, including the ability to encode generalized algebraic data types and intensional type analysis. The main contributions of this work are in the formulation of constraint types and a proof of strong normalization for an extension of System F with constraint types.en_US
dc.language.isoen_USen_US
dc.publisherBoston University Computer Science Departmenten_US
dc.relation.ispartofseriesBUCS Technical Reports;BUCS-TR-2007-015en_US
dc.titleSystem F with Constraint Typesen_US
dc.typeTechnical Reporten_US
etd.degree.nameMaster of Arts
etd.degree.levelmasters
etd.degree.disciplineComputer Science
etd.degree.grantorBoston University


Files in this item

This item appears in the following Collection(s)

Show simple item record