Source Code of a few Reduction Functions
Computing with pure lambda-terms:
Definition of pure lambda-terms
Source of reduction functions using substitution
Source of the KAM and KN
Computing with mutable terms (directed acyclic graphs):
Definition and basic operations on Explicit Substitutions
, and its
interface
Definition of mutable terms with explicit shifts
Source of the reduction of Coq V6.2
Source of the lazy abstract machine
Applications:
Bench based on Church numbers and other examples
Testing the Objective Caml machine
How to start a toplevel with KAM and LAZY ready to run (versions with statistics):
$ ocaml
Objective Caml version 1.07
# #use "use.ml";;
< lots of definitions >
# tmult nlazy 100 100;;
- : Terms.lambda = '10000
