More Web Proxy on the site http://driver.im/

article

Free access

The duality of computation

Authors:

Pierre-Louis Curien,

Hugo HerbelinAuthors Info & Claims

ACM SIGPLAN Notices, Volume 35, Issue 9

Pages 233 - 243

https://doi.org/10.1145/357766.351262

Published: 01 September 2000 Publication History

Abstract

We present the μ -calculus, a syntax for λ-calculus + control operators exhibiting symmetries such as program/context and call-by-name/call-by-value. This calculus is derived from implicational Gentzen's sequent calculus LK, a key classical logical system in proof theory. Under the Curry-Howard correspondence between proofs and programs, we can see LK, or more precisely a formulation called LK_μ, as a syntax-directed system of simple types for μ -calculus. For μ -calculus, choosing a call-by-name or call-by-value discipline for reduction amounts to choosing one of the two possible symmetric orientations of a critical pair. Our analysis leads us to revisit the question of what is a natural syntax for call-by-value functional computation. We define a translation of λμ-calculus into μ -calculus and two dual translations back to λ-calculus, and we recover known CPS translations by composing these translations.

References

[1]

F. Barbanera and S. Berardi 1996. A symmetric A-calculus for classical" program extraction. Information and Computation 125, 103-117.

Digital Library

[2]

T. Crolard 1999. Typage des coroutines en logique soustractive. In Proc. Journees Francophones des Langages Applicatifs, Collection Didactique, INRIA (http://pauillac.inria.fr/j a99).

[3]

P.-L. Curien and H. Herbelin 1998. Computing with Abstract Bohm Trees. In Proceedings of the 3rd Fuji International Symposium on Functional and Logic Programming, Eds M. Sato & Y. Toyama, World Scientific, 20-39.

[4]

V. Danos 1999. Sequent Calculus and Continuation Passing Style Compilation. To appear in Proc. of the 11th Congress of Logic, Methodology and Philosophy of Science, held in Cracow, Kluwer.

[5]

V. Danos, J.-B. Joinet and H. Schellinx 1995. LKQ and LKT: sequent calculi for second order logic based upon dual linear decompositions of classical implication. In Advances in Linear Logic, Cambridge University Press, 211-224.

Digital Library

[6]

V. Danos, J.-B. Joinet and H. Schellinx 1997. A New Deconstructive Logic: Linear Logic. In Journal of Symbolic Logic 62(3), 755-807.

[7]

V. Danos and L. Regnier 1990. Machina ex deo, ou encore quelque chose a dire sur la machine de Krivine. Unpublished.

[8]

A. Filinski 1989. Declarative Continuations: An Investigation of Duality in Programming Language Semantics. In Proc. of Category Theory and Computer Science (CTCS), LNCS 389, 224{249.

Digital Library

[9]

G. Gentzen 1935. Investigations into logical deduction. E.g. in Gentzen collected works, EdM.E. Szabo, North Holland, 68 (1969).

[10]

J.-Y. Girard 1993. On the unity of logic. Annals of Pure and Applied Logic 59, 201-217.

[11]

Ph. de Groote 1994. On the relation between the A-calculus and the syntactic theory of control. In Proc. of the International Conference onLogic Programming and Automated Reasoning (LPAR), Lecture Notes in Computer Science 822, 31-43.

Digital Library

[12]

H. Herbelin 1994. A lambda-calculus structure isomorphic to sequent calculus structure. In Proc. of Computer Science Logic (CSL), Lecture Notes in Computer Science 933, 61-75.

Digital Library

[13]

H. Herbelin 1995. Sequents qu'on calcule, Th~ese de Doctorat, Universitie Paris 7.

[14]

K. Honda and N.Yoshida 1997. Game-theoretic analysis of call-by-value computation. In Proc. of International Colloquium on Automata Languages and Programs (ICALP), Lecture Notes in Computer Science 1256.

Digital Library

[15]

M. Hofmann and T. Streicher 1997. Continuation models are universal for A-calculus. In Proc. of Logic in Computer Science (LICS), 387-397.

Digital Library

[16]

O. Laurent 1999. Polarized proof-nets and A-calculus. Draft

[17]

C. H. L. Ong and C. A. Stewart 1997. A Curry-Howard Foundation for functional computation with control. In Proc. of ACM SIGPLAN-SIGACT Symposium on Principle of Programming Languages (POPL), Paris, ACM Press, January.

Digital Library

[18]

I. Ogata 1999. Constructive Classical Logic as CPS-calculus. To appear in International Journal of Foundations of Functional Programming.

Digital Library

[19]

M. Parigot 1992. A-calculus: An algorithmic interpretation of classical natural deduction. In Proc. of the International Conference on Logic Programming and Automated Reasoning (LPAR), St.Petersburg, Lecture Notes in Computer Science 624.

Digital Library

[20]

G. D. Plotkin 1975. Call-by-name, call-by-value and the lambda-calculus. Theoretical Computer Science 1, 125-159.

Cited By

Choudhury VGay S(2025)The Duality of λ-AbstractionProceedings of the ACM on Programming Languages10.1145/37048489:POPL(332-361)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704848
Binder DTzschentke MMüller MOstermann K(2024)Grokking the Sequent Calculus (Functional Pearl)Proceedings of the ACM on Programming Languages10.1145/36746398:ICFP(395-425)Online publication date: 15-Aug-2024
https://doi.org/10.1145/3674639
Liang CMiller D(2024)Focusing Gentzen’s LK Proof SystemPeter Schroeder-Heister on Proof-Theoretic Semantics10.1007/978-3-031-50981-0_9(275-313)Online publication date: 13-Feb-2024
https://doi.org/10.1007/978-3-031-50981-0_9
Show More Cited By

Recommendations

The duality of computation
ICFP '00: Proceedings of the fifth ACM SIGPLAN international conference on Functional programming

We present the μ -calculus, a syntax for λ-calculus + control operators exhibiting symmetries such as program/context and call-by-name/call-by-value. This calculus is derived from implicational Gentzen's sequent calculus LK, a key classical ...
Duality in Some Intuitionistic Paraconsistent Logics
ICAART 2016: Proceedings of the 8th International Conference on Agents and Artificial Intelligence

Duality in constructive (or intuitionistic) logics is an important basic property since the dual counterpart of

a given constructive logic can obtain a refutation or falsification of the information or knowledge which is

described by the given logic. In ...
Classical call-by-need and duality
TLCA'11: Proceedings of the 10th international conference on Typed lambda calculi and applications

We study call-by-need from the point of view of the duality between call-by-name and call-by-value. We develop sequent-calculus style versions of call-by-need both in the minimal and classical case. As a result, we obtain a natural extension of call-by-...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 35, Issue 9

Sept. 2000

291 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/357766

Editors:
Cindy Norris
Appalachian State Univ., Boone, NC
,
James B. Fenwick
Appalachian State Univ., Boone, NC

Issue’s Table of Contents

ICFP '00: Proceedings of the fifth ACM SIGPLAN international conference on Functional programming
September 2000
294 pages
ISBN:1581132026
DOI:10.1145/351240
Chairmen:
Martin Odersky
EPFL Lausanne
,
Philip Wadler
Bell Labs, Lucent Technologies

Copyright © 2000 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 September 2000

Published in SIGPLAN Volume 35, Issue 9

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

293
Total Citations
View Citations
1,385
Total Downloads

Downloads (Last 12 months)306
Downloads (Last 6 weeks)45

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Choudhury VGay S(2025)The Duality of λ-AbstractionProceedings of the ACM on Programming Languages10.1145/37048489:POPL(332-361)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704848
Binder DTzschentke MMüller MOstermann K(2024)Grokking the Sequent Calculus (Functional Pearl)Proceedings of the ACM on Programming Languages10.1145/36746398:ICFP(395-425)Online publication date: 15-Aug-2024
https://doi.org/10.1145/3674639
Liang CMiller D(2024)Focusing Gentzen’s LK Proof SystemPeter Schroeder-Heister on Proof-Theoretic Semantics10.1007/978-3-031-50981-0_9(275-313)Online publication date: 13-Feb-2024
https://doi.org/10.1007/978-3-031-50981-0_9
Adhikary RLodhavia DFrancis CPatil RSrivastava TKhanna PBatra NBreda JPeplinski JPatel S(2023)SpiroMask: Measuring Lung Function Using Consumer-Grade MasksACM Transactions on Computing for Healthcare10.1145/35701674:1(1-34)Online publication date: 27-Feb-2023
https://dl.acm.org/doi/10.1145/3570167
Dou PZeng YWang ZHu H(2023)Multiple Temporal Pooling Mechanisms for Weakly Supervised Temporal Action LocalizationACM Transactions on Multimedia Computing, Communications, and Applications10.1145/356782819:3(1-19)Online publication date: 25-Feb-2023
https://dl.acm.org/doi/10.1145/3567828
Wu JZhu TZhu JLi TWang C(2023)A Optimized BERT for Multimodal Sentiment AnalysisACM Transactions on Multimedia Computing, Communications, and Applications10.1145/356612619:2s(1-12)Online publication date: 17-Feb-2023
https://dl.acm.org/doi/10.1145/3566126
Cantor AStump A(2023)Dual counterpart intuitionistic logicJournal of Logic and Computation10.1093/logcom/exad019Online publication date: 11-Sep-2023
https://doi.org/10.1093/logcom/exad019
Pagès R(2022)Factoring differential operators over algebraic curves in positive characteristicACM Communications in Computer Algebra10.1145/3572867.357287656:2(60-63)Online publication date: 23-Nov-2022
https://dl.acm.org/doi/10.1145/3572867.3572876
Tabuguia BKoepf W(2022)FPS in actionACM Communications in Computer Algebra10.1145/3572867.357287356:2(46-50)Online publication date: 23-Nov-2022
https://dl.acm.org/doi/10.1145/3572867.3572873
Eder CLairez PMohr RDin M(2022)Towards signature-based gröbner basis algorithms for computing the nondegenerate locus of a polynomial systemACM Communications in Computer Algebra10.1145/3572867.357287256:2(41-45)Online publication date: 23-Nov-2022
https://dl.acm.org/doi/10.1145/3572867.3572872
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Figures

Tables

Media

View Issue’s Table of Contents