OpenBU

System F with Constraint Types

OpenBU

Show simple item record

dc.contributor.author Donnelly, Kevin en_US
dc.date.accessioned 2011-10-20T04:42:48Z
dc.date.available 2011-10-20T04:42:48Z
dc.date.issued 2007 en_US
dc.identifier.uri http://hdl.handle.net/2144/1692
dc.description.abstract System 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.iso en_US en_US
dc.publisher Boston University Computer Science Department en_US
dc.relation.ispartofseries BUCS Technical Reports;BUCS-TR-2007-015 en_US
dc.title System F with Constraint Types en_US
dc.type Technical Report en_US
etd.degree.name Master of Arts
etd.degree.level masters
etd.degree.discipline Computer Science
etd.degree.grantor Boston University


Files in this item

This item appears in the following Collection(s)

Show simple item record

Search OpenBU


Browse

Deposit Materials

Statistics