- Authors:
- 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
- Publisher:
- Springer-VS
- Submission year:
- 2013
- Scientific Level:
- Scientific
- ID:
- 2185923074
Checking for on-site access...
