Typed self-representation

Self-representation – the ability to represent programs in their own language – has important applications in reflective languages and many other domains of programming language design. Although approaches to designing typed program representations for sublanguages of some base language have become quite popular recently, the question whether a fully metacircular typed selfrepresentation is possible is still open. This paper makes a big step towards this aim by defining the F∗ ω calculus, an extension of the higher-order polymorphic lambda calculus Fω that allows typed self-representations. While the usability of these representations for metaprogramming is still limited, we believe that our approach makes a significant step towards a new generation of reflective languages that are both safe and efficient. Categories and Subject Descriptors D.3.1 [Programming Languages]: Formal Definitions and Theory General Terms Languages, Theory Keywords Lambda Calculus, Language Desi...

• Type: Conference
• Year: 2009
• Where: PLDI
• Authors: Tillmann Rendel, Klaus Ostermann, Christian Hofer
• Keywords: Lambda Calculus, PLDI 2009, Programming Languages, Reflective Languages