 |
A Universe of Binding and Computation
Daniel Licata and Robert Harper
The 14th ACM SIGPLAN International Conference on Functional Programming (ICFP 2009)Edinburgh, Scotland, 31st August - 2nd September 2009
Abstract
In this paper, we construct a logical framework supporting datatypes that mix binding and computation, implemented as a universe in the dependently typed programming language Agda 2. We represent binding pronominally, using well-scoped de Bruijn indices, so types can be used to reason about the scoping of variables. We equip our universe with datatype-generic implementations of weakening, substitution, exchange, contraction, and subordination-based strengthening, so that programmers are provided these operations for free for each language they define. In our mixed, pronominal setting, weakening and substitution hold only under some conditions on types, but we show that these conditions can be discharged automatically in many cases. Finally, we program a variety of standard difficult test cases from the literature, such as normalization-by-evaluation for the untyped lambda-calculus, demonstrating that we can express detailed invariants about variable usage in a program's type while still writing clean and clear code.
START Conference Manager (V2.56.8 - Rev. 748M)