A Modern Implementation of Cut Elimination for Classical Sequent Calculus
The symmetrical properties of the sequent calculus make it an interesting base for functional programming languages. In contrast to the prevalent base lambda calculus, it allows for an equivalent treatment of terms producing information and evaluation contexts. In this thesis, we have constructed and implemented a term language for the sequent calculus, along with its cut-free fragment. We further present a normalization function that evaluates statements to their cut-free form, utilizing cut elimination and hereditary substitution. Thereby, it lends itself as a compiler intermediate language, shifting computation from runtime to compile-time, and optimizing program execution.