System F with Constraint Types


Show simple item record Donnelly, Kevin en_US 2011-10-20T04:42:48Z 2011-10-20T04:42:48Z 2007 en_US
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 Master of Arts masters Computer Science Boston University

Files in this item

This item appears in the following Collection(s)

Show simple item record

Search OpenBU


Deposit Materials