Welcome to B621
Welcome to b621.
See the bottom of notes for the April 11th exercise.
The specification from Gary Leavens can be found by taking the URL of this page and adding the charaters: l, e, a, v, e, n, s to the end of the URL.
I added a new solutions page (check menu link) where all the new work can be linked. - Roshan
Office: LH 230A
Office Hours: TBA
Textbooks and References
Download this for home use:
If you're using an O.S. (e.g., GNU/Linux on PPC) that Chez doesn't support, you can use:
and compile it yourself
Feel free to use
match, which you can find
—proof assistant for the intuitionistic sequent calculus
—handy Emacs mode for interacting with Coq, Isabelle, etc.
(inference rules / examples )
the half-finished "everything's a bird" challenge problem!
—typed, imperative / functional language (you'll need this if you wish to compile Coq)
—if you want to do any O'Caml programming, this gives comprehensive documentation of the language, the standard library, and O'CamlLex / O'CamlYacc
for Emacs (alternately, there's
If you're using a Debian-based system (this works with Ubuntu GNU/Linux, at least), you can save a lot of trouble by installing everything via: "sudo apt-get install coq proofgeneral-coq"