Document Open Access Logo

A Curry-Howard Correspondence for Linear, Reversible Computation

Authors Kostia Chardonnet, Alexis Saurin, Benoît Valiron

PDF
Thumbnail PDF

File

LIPIcs.CSL.2023.13.pdf
  • Filesize: 0.89 MB
  • 18 pages

Document Identifiers

Author Details

Kostia Chardonnet
  • Université Paris-Saclay, Inria, CNRS, ENS Paris-Saclay, LMF, 91190, Gif-sur-Yvette, France
  • Équipe Quacs, Inria, Palaiseau, France
  • Université Paris Cité, CNRS, IRIF, 75013, Paris, France
Alexis Saurin
  • Université Paris Cité, CNRS, IRIF, 75013, Paris, France
  • Inria $π r^2$, Paris, France
Benoît Valiron
  • Université Paris-Saclay, Inria, CentraleSupélec, CNRS, ENS Paris-Saclay, LMF, 91190, Gif-sur-Yvette, France

Funding

This work has been partially funded by the French National Research Agency (ANR) under the research projects SoftQPRO ANR17-CE25-0009-02 and RECIPROG ANR-21-CE48-019-01 and within the framework of "Plan France 2030", under the research project ANR-22-PETQ-0007.

Cite AsGet BibTex

Kostia Chardonnet, Alexis Saurin, and Benoît Valiron. A Curry-Howard Correspondence for Linear, Reversible Computation. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CSL.2023.13

Abstract

In this paper, we present a linear and reversible programming language with inductives types and recursion. The semantics of the languages is based on pattern-matching; we show how ensuring syntactical exhaustivity and non-overlapping of clauses is enough to ensure reversibility. The language allows to represent any Primitive Recursive Function. We then give a Curry-Howard correspondence with the logic μMALL: linear logic extended with least fixed points allowing inductive statements. The critical part of our work is to show how primitive recursion yields circular proofs that satisfy μMALL validity criterion and how the language simulates the cut-elimination procedure of μMALL.

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
  • Theory of computation → Equational logic and rewriting
Keywords
  • Reversible Computation
  • Linear Logic
  • Curry-Howard

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. David Baelde. Least and greatest fixed points in linear logic. ACM Transactions on Computational Logic (TOCL), 13(1):1-44, 2012. Google Scholar
  2. David Baelde, Amina Doumane, Denis Kuperberg, and Alexis Saurin. Bouncing Threads for Circular and Non-Wellfounded Proofs: Towards Compositionality with Circular Proofs, pages 1-13. Association for Computing Machinery, New York, NY, USA, 2022. URL: https://doi.org/10.1145/3531130.3533375.
  3. David Baelde, Amina Doumane, and Alexis Saurin. Infinitary Proof Theory: the Multiplicative Additive Case. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), volume 62 of Leibniz International Proceedings in Informatics (LIPIcs), pages 42:1-42:17, Dagstuhl, Germany, 2016. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.42.
  4. Henk Barendregt. The lambda calculus: its syntax and semantics. Studies in logic and the foundations of Mathematics, 1984. Google Scholar
  5. Yves Bertot and Pierre Castéran. Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions. Springer Science & Business Media, 2013. Google Scholar
  6. Kostia Chardonnet, Louis Lemonnier, and Benoît Valiron. Categorical semantics of reversible pattern-matching. In Ana Sokolova, editor, Proceedings 37th Conference on Mathematical Foundations of Programming Semantics, Hybrid: Salzburg, Austria and Online, 30th August - 2nd September, 2021, volume 351 of Electronic Proceedings in Theoretical Computer Science, pages 18-33. Open Publishing Association, 2021. URL: https://doi.org/10.4204/EPTCS.351.2.
  7. Haskell B Curry. Functionality in combinatory logic. Proceedings of the National Academy of Sciences, 20(11):584-590, 1934. Google Scholar
  8. Edward Fredkin and Tommaso Toffoli. Conservative logic. International Journal of theoretical physics, 21(3):219-253, 1982. Google Scholar
  9. Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C Pierce. Linear dependent types for differential privacy. In Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 357-370, 2013. Google Scholar
  10. William A Howard. The formulae-as-types notion of construction. To HB Curry: essays on combinatory logic, lambda calculus and formalism, 44:479-490, 1980. Google Scholar
  11. Rosham P. James and Amr Sabry. Theseus: A high-level language for reversible computing. Draft, available at https://legacy.cs.indiana.edu/~sabry/papers/theseus.pdf, 2014.
  12. Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. Rustbelt: Securing the foundations of the rust programming language. Proceedings of the ACM on Programming Languages, 2(POPL):1-34, 2017. Google Scholar
  13. Robin Kaarsgaard and Mathys Rennela. Join inverse rig categories for reversible functional programming, and beyond, 2021. Draft, available at URL: https://arxiv.org/abs/2105.09929.
  14. Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107-115, 2009. Google Scholar
  15. Kenji Maillard, Cătălin Hriţcu, Exequiel Rivas, and Antoine Van Muylder. The next 700 relational program logics. Proceedings of the ACM on Programming Languages, 4(POPL):1-33, 2019. Google Scholar
  16. Kenichi Morita and Yoshikazu Yamaguchi. A universal reversible turing machine. In International Conference on Machines, Computations, and Universality, pages 90-98. Springer, 2007. Google Scholar
  17. Luca Paolini, Mauro Piccolo, and Luca Roversi. A class of recursive permutations which is primitive recursive complete. Theoretical Computer Science, 813:218-233, 2020. URL: https://www.sciencedirect.com/science/article/pii/S0304397519307558.
  18. John C Reynolds. Separation logic: A logic for shared mutable data structures. In Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pages 55-74. IEEE, 2002. Google Scholar
  19. Hartley Rogers Jr. Theory of recursive functions and effective computability. MIT press, 1987. Google Scholar
  20. Amr Sabry, Benoit Valiron, and Juliana Kaizer Vizzotto. From symmetric pattern-matching to quantum control. In Christel Baier and Ugo Dal Lago, editors, Proceedings of the 21st International Conference on Foundations of Software Science and Computation Structures (FOSSACS'18), volume 10803 of Lecture Notes in Computer Science, pages 348-364, Thessaloniki, Greece, 2018. Springer. URL: https://doi.org/10.1007/978-3-319-89366-2_19.
  21. Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, et al. Dependent types and multi-monadic effects in f. In Proceedings of the 43rd annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 256-270, 2016. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact