The correspondence between proving theorems and writing programs, known as the Curry-Howard isomorphism or the proofs-as-programs paradigm, has spurred the development of new tools like proof assistants, new fields like certified programming, and new advanced type features like dependent types. The isomorphism gives us a correspondence between Gentzen's natural deduction, a system for formalizing common mathematical reasoning, and Church's λ ‐ calculus, one of the first models of computation and the foundation for functional programming languages. However, concepts found in modern programming, such as the provision of computational effects, combination of different programming paradigms and evaluation strategies, and definition of infinite objects still lack a strong foundation.

In the hopes of gaining a better understanding of these issues, we will look at an alternate form of logic, called the sequent calculus, through the Curry-Howard lens. Doing so leads us to a method of computation that heavily emphasizes the concept of duality and the interaction between opposites ‐ production interacts with consumption; construction interacts with deconstruction. The symmetry of this framework naturally explains more complicated features of programming languages through relatively familiar concepts ‐ binding a value to a variable is dual to manipulation over the flow of control in a program; case analysis over data structures in the functional paradigm is dual to dynamic dispatch in the object-oriented paradigm.

In this report, we survey the background of the connections between proofs and programs along with more modern advances. We begin by reviewing the traditional form of the Curry-Howard isomorphism that connect proof theory, category theory, and type theory, and has roots in the beginnings of computer science. We introduce the sequent calculus as an alternative form of logic, and show how the Curry-Howard isomorphism still applies and presents a different basis for expressing computation. We then show how the fundamental dilemma in the sequent calculus gives rise to a duality between evaluation strategies: strict languages are dual to lazy languages. Next, we discuss concepts that were developed in the setting of proof search, polarization and focalization, which give a foundation for data structures and pattern matching in programming languages. Taking a step back, we give a retrospective look at the history of these developments, and illustrate a generalized theory that unifies the different systems for the sequent calculus and more closely matches actual programming languages. Finally, we consider the long road ahead for using the sequent calculus as a basis for understanding programming, and discuss various future directions remaining in this line of work.