Implementing the Calculus of Constructions in Java

    For a while, I had been wondering how to do logic in the untyped lambda calculus.  It seems like that leads to paradoxes.  So I decided to go back to doing logic based on type theory, and ported my  implementation of Coquand and Huet's Calculus of Constructions (which I implemented in Prolog in Benjamin Peirce's CSE 700 class) to Java.  I hoped that this would run faster, be easier to develop a proving GUI in, and be a better platform for automated searches for proofs (which will be CPU-intensive.)
    There is a typechecker applet, which allows you to find the type of a term.  There are some example functions which should typecheck OK at the bottom of that page.
    There is also an attempt at a prover applet, which attempts to find a term of a given type (which corresponds to a proof of a given formula.)  It's somewhat primitive.
    The implementation makes use of JavaCup and JLex, both of which are written (and copyrighted by) some folks at, or formerly at, Princeton University.  Thanks partly to these, it's only about 3000 lines of Java (if you don't count the code in these components, or code generated by them.)
   There is no user documentation for it at the moment, although the source code is heavily commented, and has javadoc-generated API descriptions.  The source code is distributed under a FreeBSD-style license.  (Although later versions may be GPLed, this version is licensed in the FreeBSD style.)  This source .tar.gz archive has JavaCup and JLex bundled with it.

goals

    Ideally, I'd like to end up with a compiler for a language which has, for instance, a type:

Codec = {
    compress : String -> String
    decompress : String -> String
    works : forall s:String . (decompress (compress s)) = s
}

and a proof tool which makes finding a term of type "works" not too painful.  (A term of type "works" would mean that if you take a String, compress it, then decompress it, you get back the same String, which is what you'd like any lossless Codec to do.)
    Also, I'd like a compiler for the language which generates near-C-speed code.

References

     These are related links about strongly-typed compilers and theorem provers.  I referred to pretty much all of them in the course of writing this.

languages

Cayenne - similar to Haskell, but with a type system strong enough to encode proofs of correctness.
Haskell - the standard "lazy" strongly-typed language
Java - even if its type system isn't perfect, it gets some credit for being a decent platform for implementing all of this.

theorem provers, proof checkers, and type theory

Automath - a recent C re-implementation of de Bruijn's Automath language
Coq, Lego, Typelab - well-developed theorem provers, using propositions-as-types to represent proofs
HOL-Light - uses the HOL-LCF style of representing proofs.  Smaller and arguably cleaner than HOL.
Proof-Carrying Code - probably the closest to demonstrating "real-world" usefulness


Josh Burdick / jburdick@gradient.cis.upenn.edu / last modified November 22, 2000