When & Where: 12:30pm, Monday, June 3, 2002, Room 400 AKW
Abstract:
Multi-stage programming languages provide constructs for the construction, combination, and execution of delayed computations. At the untyped level, these languages are a unifying framework for the essence of partial evaluation, program generation, runtime code generation, and generative macro-systems. But up until now, this was not the case for the typed setting, as there have been different, orthogonal proposals for typing multi-stage languages. In fact, ever since the inception versions of these formalisms, including those of Nielson and Nielson on one hand, and Gomard and Jones on the other, the question of whether these languages should support either open code or closed code has been a challenge. Languages supporting open code admit a form of symbolic computation naturally. Languages supporting closed code allow for runtime execution of this code. Combining the two notions has been the goal of numerous previous works. Each of these works allows the typing of incomprable classes of terms.
This talk reports on two new approaches to combining open and closed code. Both these approaches subsume previous ones, and yield new insights into the problem of typing multi-stage languages.
Both proposals are based on making parameterizing the code type to provide information about the free variables in the term. The first proposal uses a system akin to de Bruijn levels to keep track of free variables in code types. The second proposal uses parametricity-like properties.
Joint work with Walid Taha.