Typed self-interpretation by pattern matching
- Publication Type:
- Conference Proceeding
- Citation:
- ACM SIGPLAN Notices, 2011, 46 (9), pp. 247 - 258
- Issue Date:
- 2011-09-01
Closed Access
| Filename | Description | Size | |||
|---|---|---|---|---|---|
 | 2011001714OK.pdf | 1.17 MB |
Copyright Clearance Process
- Recently Added
- In Progress
- Closed Access
This item is closed access and not available.
Self-interpreters can be roughly divided into two sorts: self-recognisers that recover the input program from a canonical representation, and self-enactors that execute the input program. Major progress for statically-typed languages was achieved in 2009 by Rendel, Ostermann, and Hofer who presented the first typed selfrecogniser that allows representations of different terms to have different types. A key feature of their type system is a type:type rule that renders the kind system of their language inconsistent. In this paper we present the first statically-typed language that not only allows representations of different terms to have different types, and supports a self-recogniser, but also supports a selfenactor. Our language is a factorisation calculus in the style of Jay and Given-Wilson, a combinatory calculus with a factorisation operator that is powerful enough to support the pattern-matching functions necessary for a self-interpreter. This allows us to avoid a type:type rule. Indeed, the types of System F are sufficient. We have implemented our approach and our experiments support the theory. Copyright © 2011 ACM.
Please use this identifier to cite or link to this item: