When: Thursday, June 13, 1:30 p.m.

Where: 5409 Wean Hall

Aleksandar Nanevski

Thesis Proposal

Abstract:
Meta-programming languages provide infrastructure for generation and execution of object programs at run-time. In a typed setting, they contain a modal type constructor which classifies object code. These code types generally come in two flavors: closed and open. Closed code expressions can be invoked at run-time, but the computations over them are more rigid, and typically produce less efficient residual object programs. Open code provides better inlining and partial evaluation of object programs, but once constructed, expressions of this type cannot be evaluated.

Recent work in this area has focused on combining the two notions into a sound system based on the extensions of a temporal lambda calculus. The proposed solutions are rather complex and hard to extend, and in particular, do not provide for the important operation of intensional code analysis, i.e. ability of programs to inspect and destruct object code at run-time in a type-safe manner.

My thesis in this proposal is that modal logic, specifically its necessitation fragment, together with the nominal logic concept of names, is an appropriate foundation for the notion of open code and for typed functional meta-programming with intensional code analysis. To substantiate the claim, I present a first step towards a programming language that integrates the described properties.

Thesis Committee:
Frank Pfenning (chair)
Dana Scott
Robert Harper
Peter Lee
Andrew Pitts (University of Cambridge)

<< Back