Twelf Examples

• alloc-sem.tgz (README)

  Simply Typed Lambda-Calculus with a small-step, allocation semantics.

• substruct.tgz

  Substructural Lambda-Calculus

• URAL.tgz

  Successively richer URAL qualified languages:

  • coreURAL: A formalization of the language described in Section 2 of "A Step-Indexed Model of Substructrual State", further extended to an allocation semantics.
  • refURAL: A formalization of the language described in Section 3 of "A Step-Indexed Model of Substructrual State", also extended to an allocation semantics. This language subsumes coreURAL.
  • rgnURAL: A formalization of the language described in Section 3 of "Linear Regions Are All You Need", also extended to an allocation semantics. This language subsumes rerURAL (under a suitable translation).