Name
Abstract | ||
|---|---|---|
This paper explores the surprisingly rich design space for the simply typed lambda calculus with casts and a dynamic type. Such a calculus is the target intermediate language of the gradually typed lambda calculus but it is also interesting in its own right. In light of diverse requirements for casts, we develop a modular semantic framework, based on Henglein's Coercion Calculus, that instantiates a number of space-efficient, blame-tracking calculi, varying in what errors they detect and how they assign blame. Several of the resulting calculi extend work from the literature with either blame tracking or space efficiency, and in doing so reveal previously unknown connections. Furthermore, we introduce a new strategy for assigning blame under which casts that respect traditional subtyping are statically guaranteed to never fail. One particularly appealing outcome of this work is a novel cast calculus that is well-suited to gradual typing. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/978-3-642-00590-9_2 | ESOP |
Keywords | Field | DocType |
computer science,higher order,typed lambda calculus,dynamic typing,intermediate language | Normalisation by evaluation,Simply typed lambda calculus,Typed lambda calculus,Lambda cube,Computer science,System F,Theoretical computer science,Pure type system,Dependent type,Process calculus | Conference |
Volume | ISSN | Citations |
5502 | 0302-9743 | 28 |
PageRank | References | Authors |
1.32 | 7 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jeremy G. Siek | 1 | 563 | 45.96 |
| Ronald Garcia | 2 | 139 | 13.53 |
| Walid Taha | 3 | 1020 | 70.41 |