Recovered source · 2003–2004
Binding structures, in working examples.
These files were distributed with or linked from the original Fresh OCaml site. They use syntax specific to the historical compiler and are presented unchanged as research artifacts.
A.M. Pitts · 2003
Normalization by evaluation
Untyped lambda terms represented with Fresh OCaml names and abstraction types.
Open complete sourcetype t;;
type var = t name;;
type term =
Var of var
| Lam of <<var>>term
| App of term * term;;
let rec reify d =
match d with
L f ->
let x = fresh in
Lam(<<x>>(reify(f(function () -> N(V x)))))
| N n -> reifyn n;;Complete example set