This is a type checker for a small dependently typed language.

The type checker implements the algorithm from Thierry Coquand's
An Algorithm for Type-Checking Dependent Types, available at:
http://www.cs.chalmers.se/~coquand/type.ps

Requirements:

- Java 1.5, available from:
  http://java.sun.com/j2se/1.5.0/download.jsp

- The Java CUP runtime classes should be on your CLASSPATH.
  They are available from:
  http://www.cs.princeton.edu/~appel/modern/java/CUP/

Compilation:

$ make

Usage:

The Test program reads judgements on the form "Exp : Exp" from
standard input and checks whether the first term has the type given
byt the second term.

$ make test

Example:

(user enters "(\A -> \x -> x) : (A:Type)(x:A)A")

$ make test
(\A -> \x -> x) : (A:Type)(x:A)A
\ A -> \ x -> x : (A : Type) (x : A) A => true