Proofs, upside down: a functional correspondence between natural deduction and the sequent calculus
Title: Proofs, upside down: a functional correspondence between natural deduction and the sequent calculus
Speaker: Matthias Puech (Aarhus University, Denmark)
Time: 14:00, Thursday, 19th December 2013
Venue: ____Room 337_____, Building #5, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
Abstract:
It is well known in proof theory that sequent-calculus proofs differ from natural deduction proofs by “reversing” elimination rules up-side down into left introduction rules. It is also well known that to each recursive, functional program corresponds an equivalent iterative, accumulator-passing program, where the accumulator stores the continuation of the iteration, in “reversed” order. Here, we compose these remarks and show that a restriction of the intuitionistic sequent calculus, LJT, is exactly an accumulator-passing version of intuitionistic natural deduction NJ. More precisely, we obtain this correspondence by applying a series of off-the-shelf program transformations a la Danvy et al. on a type checker for the bidirectional lambda-calculus, and get a type checker for the lambda-calculus, the proof term assignment of LJT. This functional correspondence revisits the relationship between natural deduction and the sequent calculus by systematically deriving the rules of the latter from the former, and allows us to derive new sequent calculus rules from the introduction and elimination rules of new logical connectives.
It is well known in proof theory that sequent-calculus proofs differ from natural deduction proofs by “reversing” elimination rules up-side down into left introduction rules. It is also well known that to each recursive, functional program corresponds an equivalent iterative, accumulator-passing program, where the accumulator stores the continuation of the iteration, in “reversed” order. Here, we compose these remarks and show that a restriction of the intuitionistic sequent calculus, LJT, is exactly an accumulator-passing version of intuitionistic natural deduction NJ. More precisely, we obtain this correspondence by applying a series of off-the-shelf program transformations a la Danvy et al. on a type checker for the bidirectional lambda-calculus, and get a type checker for the lambda-calculus, the proof term assignment of LJT. This functional correspondence revisits the relationship between natural deduction and the sequent calculus by systematically deriving the rules of the latter from the former, and allows us to derive new sequent calculus rules from the introduction and elimination rules of new logical connectives.
Biography:
Matthias Puech is a post-doctoral fellow in Computer Science at Aarhus University, Denmark. He obtained a Ph.D from Universite Paris Diderot working at the PPS lab, and Universita di Bologna. During his thesis, he worked in the fields of type and proof theory, namely on proof certificates, incremental type-checking and sequent calculus. His domain of interest include:
— the interaction between functional programming and the LF logical framework, in particular wrt. HOAS encodings,
— the logical interpretation of functional language transformations, in particular CPS and defunctionalization,
— the implementation of theorem provers, both automated and interactive, in particular Coq.