Publications:Exploring the Design Space of Higher-Order Casts

From CERES
Revision as of 04:44, 26 June 2014 by Slawek (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

Do not edit this section

Keep all hand-made modifications below

Title Exploring the Design Space of Higher-Order Casts
Author Jeremy Siek and Ronald Garcia and Walid Taha
Year 2009
PublicationType Conference Paper
Journal
HostPublication Programming languages and systems : 18th European symposium on programming, ESOP 2009, held as part of the joint european conferences on theory and practice of software, ETAPS 2009, York, UK : proceedings
DOI http://dx.doi.org/10.1007/978-3-642-00590-9_2
Conference 18th European Symposium on Programming, ESOP 2009; York; 22 March 2009 through 29 March 2009
Diva url http://hh.diva-portal.org/smash/record.jsf?searchId=1&pid=diva2:396151
Abstract This paper explores the surprisingly rich design space for the simplytyped lambda calculus with casts and a dynamic type. Such a calculus is the targetintermediate language of the gradually typed lambda calculus but it is alsointeresting in its own right. In light of diverse requirements for casts, we developa modular semantic framework, based on Henglein’s Coercion Calculus, that instantiatesa number of space-efficient, blame-tracking calculi, varying in whaterrors they detect and how they assign blame. Several of the resulting calculi extendwork from the literature with either blame tracking or space efficiency, andin doing so reveal previously unknown connections. Furthermore, we introduce anew strategy for assigning blame under which casts that respect traditional subtypingare statically guaranteed to never fail. One particularly appealing outcomeof this work is a novel cast calculus that is well-suited to gradual typing.