prop.{sig,sml} - propositions of intuitionistic propositional logic (IPL)
term.{sig,sml} - proof terms for IPL
check.sig      - interface to proof checker = bidirectional type checker
check.sml      - your implementation of a proof checker
g4ip.sig       - interface to certifying decision procedure for IPL
g4ip.sml       - your implementation of a certifying decision procedure

test-prop.sml  - tests, including some new interaction laws over HW5
top.sml        - scripts for running tests
                 to see/hide the proof terms, comment in/out a line in top.sml

Experimenting:

% sml
- CM.make "sources.cm";
- Top.runproofs(); (* test proof checkers *)
- Top.runtests(); (* test certifying G4ip *)
- Top.runbonus(); (* possible need to interrupt --- may time out *)
