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.
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.