^{1} Department of Computer Science, Science and Technology, Aarhus University^{2} Department of Computer Science, Science and Technology, Aarhus University

DOI:

10.1007/978-3-319-03542-0_26

Abstract:

It is well known in proof theory that sequent-calculus proofs differ from natural deduction proofs by “reversing” elimination rules upside 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 à la Danvy et al. on a type checker for the bidirectional λ-calculus, and get a type checker for the λ¯ -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.

ISBN:

9783319035420, 9783319035413

Type:

Conference paper

Language:

English

Published in:

Lecture Notes in Computer Science: 11th Asian Symposium, Aplas 2013, Melbourne, Vic, Australia, December 9-11, 2013. Proceedings, 2013, p. 365-380

Main Research Area:

Science/technology

Publication Status:

Published

Series:

Lecture Notes in Computer Science

Review type:

Peer Review

Conference:

Asian Symposium on Programming Languages and SystemsAsian Symposium on Programming Languages and Systems, 2013