A Tutorial on Computational Classical Logic and the Sequent Calculus

https://ix.cs.uoregon.edu/~pdownen/publications/sequent-intro.pdf

Paul Downen and Zena. M. Ariola
University of Oregon

We present a model of computation that heavily emphasizes the concept of duality and the interaction between opposites—production interacts with consumption. The symmetry of this framework naturally explains more complicated features of programming languages through relatively familiar concepts. For example, binding a value to a variable is dual to manipulating the flow of control in a program. By looking at the computational interpretation of the sequent calculus, we find a language that lets us speak about duality, control flow, and evaluation order in programs as first-class concepts.
We begin by reviewing Gentzen’s LK sequent calculus and show how the Curry-Howard isomorphism still applies to give us a different basis for expressing computation. We then illustrate how the fundamental dilemma of computation in the sequent calculus gives rise to a duality between evaluation strategies: strict languages are dual to lazy languages. Finally, we discuss how the concept of focusing, developed in the setting of proof search, is related to the idea of type safety for computation expressed in the sequent calculus. In this regard, we compare and contrast two different methods of focusing that have appeared in the literature, static and dynamic focusing, and illustrate how they are two means to the same end

The Logical Abstract Machine: a Curry-Howard isomorphism for machine code

http://www.riec.tohoku.ac.jp/~ohori/research/flops99.pdf

Atsushi Ohori

This paper presents a logical framework for low-level ma-
chine code and code generation. We first define a calculus, called
sequential sequent calculus, of intuitionistic propositional logic. A proof of the
calculus only contains left rules and has a linear (non-branching) struc-
ture, which reflects the properties of sequential machine code. We then
establish a Curry-Howard isomorphism between this proof system and
machine code based on the following observation. An ordinary machine
instruction corresponds to a polymorphic proof transformer that extends
a given proof with one inference step. A return instruction, which turns
a sequence of instructions into a program, corresponds to a logical ax-
iom (an initial proof tree). Sequential execution of code corresponds to
transforming a proof to a smaller one by successively eliminating the last
inference step. This logical correspondence enables us to present and an-
alyze various low-level implementation processes of a functional language
within the logical framework. For example, a code generation algorithm
for the lambda calculus is extracted from a proof of the equivalence the-
orem between the natural deduction and the sequential sequent calculus.