Semi-Axiomatic Sequent Calculus
Henry DeYoung, Frank Pfenning, Klaas Pruiksma · arXiv (Cornell University) · 2020
We present the semi-axiomatic sequent calculus (SAX) that blends features of Gentzen’s sequent calculus with an axiomatic formulation of intuitionistic logic. We develop and prove a suitable analogue to cut elimination and then show that a natural computational interpretation of SAX provides a simple form of shared memory concurrency.