COMP 321-fall 08- hw5 (candidates for final projects)

Projects are due by Dec. 14. You may work in a group, but each member of the group must turn in code in a file with his or her name at the top (as a comment) as well as the names of the group members.

All members of the group must meet with me (together) in my office to give a demo of the code No exceptions. Demos should be scheduled by the Dec.8, and must be given the week ending Dec. 14.

Prolog

  1. Implement (in Prolog) substitution and beta reduction in the untyped lambda-calculus
  2. Implement a type-checker for the simply typed lambda calculus, in Prolog
  3. Implement type-inference for the simply typed lambda calculus, in Prolog (actually, in Prolog, this might as well include the preceding problem)
  4. Implement a Prolog interpreter in Prolog with some nice features added. This is much easier than it sounds.

Prolog, ML or Java

  1. Implement unification of terms (in ML) and/or type inference.
  2. Implement an interpreter for the simply typed lambda calculus, i.e. beta-reduction to normal form. If you work in a large group you might want to dress it up to take some defined terms such as those in arithmetic, or even simple inductive definitions (then translated using Fix and then reduced).
  3. Implement a basic Prolog interpreter in ML. This is a project for a group of 4.
  4. Implement SKI complilation to combinators of the untyped lambda calculus: in more detail:

    S-K-C-B compiler

    Implement a function trans that translates an untyped closed lambda-term into an expression made up of applications of S,K,I,C,B as described in Stansifer's notes on the lambda calculus. If you work in a group, some of you may implement a leftmost evaluator of the resulting combinator term: 
        eval (S u v w) = eval (u w) (v w)
    etc.
  5. Implement a classical propositional logic theorem prover in the sequent calculus, using Wang's Algorithm.
    Last modified: Thu Dec 4 00:52:23 EST 2008