Abstract
This paper introduces the Recursive Polarized Dual Calculus (RP-DC), based on Wadler's Dual Calculus. RP-DC features a polarized form of reduction, which enables several simplifications over previous related systems. It also adds inductive types with recursion, from which coinductive types with corecursion can be defined. Typing and reduction relations are defined for RP-DC, and we consider several examples of practical programming. Logical consistency is proved, as well as a canonicity theorem showing that all closed values of a certain family of types are canonical. This shows how RP-DC can be used for practical programming, where canonical final results are required.
References
[1]
Andreas M. Abel and Brigitte Pientka. Wellfounded recursion with copatterns: a unified approach to termination and productivity. In Tarmo Uustalu, editor, Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 185--196. ACM, 2013.
[2]
Thorsten Altenkirch and Nils Anders Danielsson. Termination Checking Nested Inductive and Coinductive Types. Short note supporting a talk given at PAR 2010, Workshop on Partiality and Recursion in Interactive Theorem Provers. Available from the authors' web pages.
[3]
Andrew W. Appel. Compiling with Continuations. Cambridge University Press, 1992.
[4]
Robert Atkey and Conor McBride. Productive coprogramming with guarded recursion. In Tarmo Uustalu, editor, Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 197--208. ACM, 2013.
[5]
Marc Bezem, Keiko Nakata, and Tarmo Uustalu. On streams that are finitely red. Logical Methods in Computer Science, 8(4), 2012.
[6]
Tristan Crolard. A confluent lambda-calculus with a catch/throw mechanism. J. Funct. Program., 9(6):625--647, 1999.
[7]
Pierre Curien and Hugo Herbelin. The duality of computation. In Proceedings of the fifth ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 233--243. ACM, 2000.
[8]
Olivier Danvy and Andrzej Filinski. Abstracting control. In LISP and Functional Programming, pages 151--160, 1990.
[9]
Matthias Felleisen. The theory and practice of first-class prompts. In Jeanne Ferrante and P. Mager, editors, Fifteenth Annual ACM Symposium on Principles of Programming Languages (POPL), San Diego, California, USA, January 10-13, 1988, pages 180--190, 1988.
[10]
Timothy Griffin. A Formulae-as-Types Notion of Control. InFrances E. Allen, editor, Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages (POPL), pages 47--58. ACM Press, 1990.
[11]
Daisuke Kimura and Makoto Tatsuta. Call-by-value and call-by-name dual calculi with inductive and coinductive types. Logical Methods in Computer Science, 9(1), 2013.
[12]
Dexter Kozen. Results on the propositional λ-calculus. Theoretical Computer Science, 27(3):333--354, 1983.
[13]
Jean-Louis Krivine. Realizability in classical logic. Panoramas et synthèses, 27:197--229, 2009. Interactive models of computation and program behaviour. Société Mathématique de France.
[14]
Paul Francis Mendler. Inductive Definition in Type Theory. PhD thesis, Cornell University, 1988. Available at http://www.nuprl.org/documents/Mendler/InductiveDefinition.html.
[15]
Russell O'Connor. Classical mathematics for a constructive world. Mathematical Structures in Computer Science, 21(4):861--882, 2011.
[16]
Michel Parigot. Lambda-Mu-Calculus: An algorithmic interpretation of classical natural deduction. In Andrei Voronkov, editor, Logic Programming and Automated Reasoning, pages 190--201, 1992.
[17]
Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strnisa. Ott: Effective tool support for the working semanticist. J. Funct. Program., 20(1):71--122, 2010.
[18]
Philip Wadler. Call-by-Value Is Dual to Call-by-Name -- Reloaded. In Jürgen Giesl, editor, Rewriting Techniques and Applications (RTA), Lecture Notes in Computer Science, pages 185--203. Springer, 2005.
Index Terms
- The recursive polarized dual calculus
Recommendations
Investigations on the Dual Calculus
The Dual Calculus, proposed recently by Wadler, is the outcome of two distinct lines of research in theoretical computer science: (A) Efforts to extend the Curry-Howard isomorphism, established between the simply-typed lambda calculus and intuitionistic ...
Polarized proof-nets and λµ-calculus
We first define polarized proof-nets, an extension of MELL proof-nets for the polarized fragment of linear logic; the main difference with usual proof-nets is that we allow structural rules on any negative formula. The essential properties (confluence, ...
Dual Calculus with Inductive and Coinductive Types
RTA '09: Proceedings of the 20th International Conference on Rewriting Techniques and ApplicationsThis paper gives an extension of Dual Calculus by introducing inductive types and coinductive types. The same duality as Dual Calculus is shown to hold in the new system, that is, this paper presents its involution for the new system and proves that it ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
January 2014
66 pages
Copyright © 2014 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]
Sponsors
In-Cooperation
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 11 January 2014
Check for updates
Author Tags
Qualifiers
- Research-article
Conference
POPL '14
Sponsor:
POPL '14: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
January 21, 2014
California, San Diego, USA
Acceptance Rates
PLPV '14 Paper Acceptance Rate 5 of 7 submissions, 71%;
Overall Acceptance Rate 18 of 25 submissions, 72%
Upcoming Conference
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 76Total Downloads
- Downloads (Last 12 months)2
- Downloads (Last 6 weeks)0
Reflects downloads up to 11 Jan 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in