Skip Navigation

Document Information

Second-Order Classical Sequent Calculus
Philip Johnson-Freyd
Committee: Zena Ariola (chair), Michal Young, Boyana Norris, Robert Armstrong (Sandia National Laboratories), Geoffrey Hulette (Sandia National Laboratories)
Directed Research Project(Oct 2014)
Keywords: Programming Languages, Classical Logic, Control, Second Order Logic, Polymorphism

We present a sequent calculus that allows to abstract over a type variable. The introduction of the abstraction on the right-hand side of a sequent corresponds to the universal quantification; whereas, the introduction of the abstraction on the left-hand side of a sequent corresponds to the existential quantification. The calculus provides a correspondence with second-order classical propositional logic. To show consistency of the logic and consequently of the type system, we prove the property of strong normalization. The proof is based on an extension of the reducibility method, consisting of associating to each type two sets: a set of of strong normalizing terms and a set of strong normalizing co-terms.