Hirrolot

(* The syntax of our calculus. Notice that types are represented in the same way
   as terms, which is the essence of CoC. *)
type term =
  | Var of string
  | Appl of term * term
  | Binder of binder * string * term * term
  | Star
  | Box

and binder = Lam | Pi

jdp

#!/usr/bin/env python

import sys
import types
import operator

class Runtime:
    def __init__(self, env={}, stack=[]):
        self.env = {
            # Primitive words, not an impressive base but it works