Proofs, Upside Down - A Functional Correspondence between Natural Deduction and the Sequent Calculus
Abstract elided by the publisher.
Related papers
- Lambda terms for natural deduction, sequent calculus and cut elimination JFP 2000
- A proof theory for machine code TOPLAS 2007
- Grokking the Sequent Calculus (Functional Pearl) ICFP 2024
- Computational Types from a Logical Perspective JFP 1998
- On Polymorphic Sessions and Functions - A Tale of Two (Fully Abstract) Encodings ESOP 2018
- On Polymorphic Sessions and Functions: A Tale of Two (Fully Abstract) Encodings TOPLAS 2021
- Introduction and elimination, left and right ICFP 2022
- The duality of computation ICFP 2000