A proof of cut elimination for a boring logic in a not boring metatheory
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
README.md
cut.elf
logic.elf
sources.cfg

README.md

cut

A simple proof of cut elimination for a intuitionistic sequent calculus. The calculus has 5 connectives: implication, conjunction, disjunction, true, and false.

The file logic.elf formalizes the syntax and typing judgment for the logic and cut.elf proves cut elimination. Note that this is an extrinsic cast of the logic rather than the intrinsic version found on the Twelf wiki. Read the code for cut for a gist of how the proof works and of/cut (the actual theorem) for the gory details.