{"controller"=>"catalog", "action"=>"show", "id"=>"2185923074"}
  • EN
  • DA

Danish NationalResearch Database

  • Search Publications & Researchers
  • Open Access Indicator
  • Publications
  • Researchers
Example Finds records
water{} containing the word "water".
water supplies"{}" containing the phrase "water supplies".
author:"Doe, John"author:"{}" containing the prase "Doe, John" in the author field.
title:IEEEtitle:{} containing the word "IEEE" in the title field.
Need more help? Advanced search tutorial
  • Selected (0)
  • History

Proofs, Upside Down

    • Save to Mendeley
    • Export to BibTeX
    • Export to RIS
    • Email citation
Authors:
  • Puech, Matthias
    Close
    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:
9783319035413, 9783319035420
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

Full text access

  • Doi Get publisher edition via DOI resolver
Checking for on-site access...

On-site access

At institution

  • Aarhus university.en

Metrics

Feedback

Sitemap

  • Search
    • Statistics
    • Tutorial
    • Data
    • FAQ
    • Contact
  • Open Access
    • Overview
    • Development
    • FAQ
    • Contact
  • About
    • Institutions
    • Release History
    • Cookies and privacy policy

Copyright © 1998–2018.

Fivu en