Effectful Staging Project
       Joint work with Yukiyoshi Kameyama and Chung-chieh Shan

Staging with effects of delimited dynamic extent

     Shifting the Stage: Staging with Delimited Control
     Yukiyoshi Kameyama, Oleg Kiselyov, and Chung-chieh Shan
     PEPM 2009.

circle-shift.pdf		The paper

circle-shift.elf		lambda-circle calculus with shift/reset:
  two-stage calculus with delimited control effects.
  This Twelf code defines the calculus and its static (type checking)
  and dynamic semantics. The code contains many examples, including
  the staged Gibonacci example with memoization and let-insertion.

	Gibonacci example -- generating efficient specialized
	versions of the generalized Fibonacci function in direct style. 
	The code files below describe a progression of attempts,
	from inefficient unstaged Gibonacci, memoized Gibonacci, 
	naively staged and inefficient function and finally to the
	efficient memoization with let-insertion. The dangers of scope
	extrusion are well illustrated. The specialized Gibonacci generator
	is written in direct, rather than monadic or CPS style.
fib.ml				With the explicit fix-point combinator
fib1.ml				Without the explicit fix-point combinator
				All the code is in MetaOCaml

	Generating optimal specialized code for the longest common 
	subsequence: another example of dynamic meta-programming in 
	direct style
lcs.ml				The complete MetaOCaml code


		Generating a family of Gaussian Elimination codes
		in direct style, without either functors or monads
ge-unstaged.ml			Unstaged, textbook Gaussian elimination code,
				in OCaml
ge-gen.ml			Staged ge-unstaged.ml, in MetaOCaml.
				The staged code generates
				a family of GE codes (with or without 
				determinant computation, etc). We pay 
				no performance penalty for the added
				flexibility. 

				


Translating the staging away

     Closing the Stage: From staged code to typed closures
     Yukiyoshi Kameyama, Oleg Kiselyov, and Chung-chieh Shan
     PEPM 2008.

metafx.pdf			The paper

meta-scheme.scm			Examples of the staged code and its translation 
  This file contains the complete code for all the examples in the paper
  plus extra examples. 
  The source language is MetaOCaml. The target language is supposed to be 
  System F. We try to emulate it in plain OCaml, using first-class (record)
  polymorphism where needed.


lambda-am1.elf		The implementation of the lambda^a_{v1} calculus
  This is the two-stage calculus with run and cross-stage persistence,
  which is a close model of MetaOCaml (restricted to two stages).
  The calculus is the source language of the translation.
  This Twelf code defines the syntax, static and the dynamic semantics
  of the calculus, and proves several meta-theorems (context
  decomposition, subject reduction for primitive reductions).

power-count.ml			Specializing the power function while
 determining the number of multiplications in the generated code.
 It is easiest to write this example if we use a side effect such as
 mutable state in MetaOCaml, but such an extension (a piece of state of
 type int) has not been shown sound except through our translation. 
 Second, we can write this example in pure MetaOCaml (more awkwardly) using 
 our environment-passing translation.