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.

Solutions

I added a new solutions page (check menu link) where all the new work can be linked. - Roshan

Instructors

Dan Friedman
Email: dfried@cs.indiana.edu
Phone: 5-4885
Office: LH 230A
Office Hours: TBA

Textbooks and References

Scheme, etc.
- Download this for home use: Chez Scheme
- If you're using an O.S. (e.g., GNU/Linux on PPC) that Chez doesn't support, you can use: MZ Scheme and compile it yourself
- Feel free to use match, which you can find here.
Coq, etc.
- Coq—proof assistant for the intuitionistic sequent calculus
- Proof General—handy Emacs mode for interacting with Coq, Isabelle, etc.
- Coq slides (inference rules / examples )
- the half-finished "everything's a bird" challenge problem!
- O'Caml—typed, imperative / functional language (you'll need this if you wish to compile Coq)
  - O'Caml manual—if you want to do any O'Caml programming, this gives comprehensive documentation of the language, the standard library, and O'CamlLex / O'CamlYacc
  - Caml mode for Emacs (alternately, there's Tuareg mode)
- 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"