The code accompanying the paper
Finally Tagless, Partially Evaluated:
Tagless Staged Interpreters for Simpler Typed Languages
Copyright (c) 2007-2008, Jacques Carette, Chung-chieh Shan, Oleg Kiselyov
Overview of the files
(the files are in the same directory as this README.txt file)
Warm-up: simple tagless (and, for comparison, tag-full) interpreters
They are all in (Meta)OCaml.
tagless_interp1.ml Tagfull and tagless (staged) interpreters
for simply typed lambda-calculus with booleans,
and deBruijn encoding of variables
tagless_interp2.ml Tagless staged interpreter for simply typed lambda-
calculus with de Bruijn indices and booleans,
integers, pairs, references, sequencing and let.
tagless_interp21.ml The same as above but using higher-order
abstract syntax rather than de Bruijn indices
Warm up: simple typed tagless partial evaluators
tagless_pe3.ml For the language of tagless_interp2.ml
tagless_pe4.ml The same with CPS, distinguishing pure from
potentially effectful computations
The main development: code described in the paper
In (Meta)Ocaml:
incope.ml Tagless typed interpreters, compilers,
partial evaluators, CBV and CBN CPS
interpreters and transformers,
continuation- and state-passing interpreter
incope-dB.ml Tagless typed interpreters, compilers,
partial evaluators: using de Bruijn indices
rather than higher-order abstract syntax
inco.ml Abstracting over object language types:
bool, int, and arrow.
In Haskell:
Incope.hs Tagless typed interpreters, (byte) compilers,
partial evaluator, HOAS bytecode compiler,
various self-interpreters.
Byte-compilers use GADT to emulate safe
staging.
Tagless partial evaluator is given in two
versions: with GADT and without
incope1.hs Tagless interpreter, compiler, partial evaluator.
The partial evaluator is implemented with
typeclasses instead of GADTs.
IncopeTypecheck.hs Typechecking into Symantics terms:
conversion of untyped terms into the typed
terms that can be interpreted by various typed
interpreters.
Last updated: November 2008.