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.issued2007
dc.identifier.urihttps://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_US
dc.publisherBoston University Computer Science Departmenten_US
dc.relation.ispartofseriesBUCS Technical Reports;BUCS-TR-2007-015
dc.titleSystem F with Constraint Typesen_US
dc.typeTechnical Reporten_US
etd.degree.nameMaster of Artsen_US
etd.degree.levelmastersen_US
etd.degree.disciplineComputer Scienceen_US
etd.degree.grantorBoston Universityen_US


This item appears in the following Collection(s)

Show simple item record