Princeton University
Computer Science Department

Computer Science 598A
Automated Theorem Proving

Andrew Appel


Spring 2003

General Information | Schedule | Assignments | Announcements
Assignment 11
Write a program in Twelf that can produce safety proofs for programs that use lists.

0. Setup

Put this assignment in a file typecheck.elf.

1. Type Checker

Write a logic program lookup that looks up a variable in a list of typings, that is, lookup V TS T looks up variable V in the list of typings TS and produces a type T.

Write a logic program exptype TS E T that takes a list of typings TS, an expression E, and produces a type T. The idea is that each variable in the expression E can be looked up in TS.

Write a logic program delete TS V TS' that deletes any typings of the variable V from the list of typings TS, resulting in the list TS'.

Write a logic program check IS1 IS2 Pre C Post that type-checks a program-statement C, with respect to precondition Pre and postcondition Post, which are both lists of typings. The "difference list" IS1,IS2 is an and-separated, true-terminated list of while-loop invariants; each member of this list is a list of typings.

2. Semantic model

Write the semantic model, that is, define each of the predicates for which you wrote progams in part 1, and then prove each of the clauses as a lemma.

3. Run your program

Demonstrate that your typechecker can prove safety of programs such as reverse, as follows: 
%define post1 = Q
%solve  proof1 : check ((is_list @ q and is_list @ p and true) and true) I' 
                 (is_list @ p and true)
                 reverse
                 Q.

pf_reverse_thm: pf (reverse_thm) = 
 cut (imp_i [p1a] and_i p1a true_i)
      [p1: pf (is_list @ p imp (is_list @ p and true))]
 cut (imp_i and_e1)
      [p2: pf (post1 imp is_list @ q)]
 strengthen p1 (weaken p2 (check_e proof1)).