
- Translation between DeBruijn and HOAS
   (type preserving)

  debruijn.bel

  Nice features: use context matching
    use context as the environment to look up the
    position of a bound variable

    much easier to write the converse:
    translation of deBruijn term to HOAS
    not required to prove well-formedness of environment.

  Extension: handle polymorphism / system F

  Index debruijn terms also with a number which denotes the maximum
  number of binders


- Evaluation   (term-typed.bel)
    Types guarantee that some cases are impossible
    no error handling is necessary

- CPS translation (2 different kinds)
   cps-popl-tutorial1-crec.bel
   cps-popl-tutorial2-crec.bel

   we show two different type-preserving CPS translations
   one of them avoids administrative redeces

- Closure conversion (untyped) (conv-cheney.bel)
  Distinguishes between the context of variables occurring in the
  source language and in the target language; this would even be
  possible if we would use the same language for source and target.

  Typed closure conversion see Francois Pottier's slides.


---------------------------------------------------------------
TODO:

- Evaluator for CPS terms

- Typed closure conversion

- Extensions to handle system F

Current status:

- we have typed translations between deBruijn and HOAS
- we have typed cps translation
- we have untyped cclosure conversion
- we have a sketch of typed closure conversion


---------------------------------------------------------------

Possible extensions / Related systems :

- MinCAML: A simple and efficient compiler for a minimal functional language
   Eijiro Sumii

- From System F to typed assembly language




