摘要：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.
