Document Open Access Logo

A Certified Study of a Reversible Programming Language

Authors Luca Paolini, Mauro Piccolo, Luca Roversi

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2015.7.pdf
  • Filesize: 0.64 MB
  • 21 pages

Document Identifiers

Author Details

Luca Paolini
Mauro Piccolo
Luca Roversi

Cite AsGet BibTex

Luca Paolini, Mauro Piccolo, and Luca Roversi. A Certified Study of a Reversible Programming Language. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 7:1-7:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.TYPES.2015.7

Abstract

We advance in the study of the semantics of Janus, a C-like reversible programming language. Our study makes utterly explicit some backward and forward evaluation symmetries. We want to deepen mathematical knowledge about the foundations and design principles of reversible computing and programming languages. We formalize a big-step operational semantics and a denotational semantics of Janus. We show a full abstraction result between the operational and denotational semantics. Last, we certify our results by means of the proof assistant Matita.
Keywords
  • reversible computing
  • Janus
  • operational semantics
  • bi-deterministic evaluation
  • categorical semantics

Metrics

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

References

  1. Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi. The Matita interactive theorem prover. In Nikolaj Bjørner and Viorica Sofronie-Stokkermans, editors, Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings, volume 6803 of Lecture Notes in Computer Science, pages 64-69. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-22438-6_7.
  2. Holger Bock Axelsen and Robert Glück. What do reversible programs compute? In Martin Hofmann, editor, Foundations of Software Science and Computational Structures - 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings, volume 6604 of Lecture Notes in Computer Science, pages 42-56. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-19805-2_4.
  3. Holger Bock Axelsen, Robert Glück, and Tetsuo Yokoyama. Reversible machine code and its abstract processor architecture. In Volker Diekert, Mikhail V. Volkov, and Andrei Voronkov, editors, Computer Science - Theory and Applications, Second International Symposium on Computer Science in Russia, CSR 2007, Ekaterinburg, Russia, September 3-7, 2007, Proceedings, volume 4649 of Lecture Notes in Computer Science, pages 56-69. Springer, 2007. URL: http://dx.doi.org/10.1007/978-3-540-74510-5_9.
  4. C. H. Bennett. Logical reversibility of computation. IBM J. Res. Develop., 17(6):525-532, 1973. URL: http://dx.doi.org/10.1147/rd.176.0525.
  5. Nick Benton, Andrew Kennedy, and Carsten Varming. Some domain theory and denotational semantics in Coq. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, volume 5674 of Lecture Notes in Computer Science, pages 115-130. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-03359-9_10.
  6. R. Blute and P. Scott. Category theory for linear logicians. In T. Ehrhard, J.-Y. Girard, P. Ruet, and P. Scott, editors, Linear Logic in Computer Science, volume 316 of London Math. Soc. Lecture Note Series, pages 3-64. Cambridge University Press, 2004. URL: http://dx.doi.org/10.1017/cbo9780511550850.002.
  7. The Coq Development Team. The Coq proof assistant development manual, 2005. URL: http://coq.inria.fr/doc/main.html.
  8. R. P. James and A. Sabry. Theseus: A high level language for reversible computing, 2014. URL: http://www.cs.indiana.edu/~sabry/research.html.
  9. Roshan P. James and Amr Sabry. Isomorphic interpreters from logically reversible abstract machines. In Robert Glück and Tetsuo Yokoyama, editors, Reversible Computation, 4th International Workshop, RC 2012, Copenhagen, Denmark, July 2-3, 2012. Revised Papers, volume 7581 of Lecture Notes in Computer Science, pages 57-71. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-36315-3_5.
  10. C. Lutz. Janus, a time reversible language. Letter to R. Landauer, 1986. URL: http://www.peterhines.net/downloads/others/JANUS.html.
  11. A. Megacz. Category theory library for Coq. URL: http://www.cs.berkeley.edu/~megacz/coq-categories/.
  12. Torben Æ. Mogensen. Partial evaluation of the reversible language janus. In Siau-Cheng Khoo and Jeremy G. Siek, editors, Proceedings of the 2011 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2011, Austin, TX, USA, January 24-25, 2011, pages 23-32. ACM, 2011. URL: http://dx.doi.org/10.1145/1929501.1929506.
  13. L. Paolini, M. Piccolo, and L. Roversi. Janus formalization in Matita. URL: http://www.di.unito.it/~piccolo/janus.zip.
  14. Luca Paolini, Mauro Piccolo, and Luca Roversi. A class of reversible primitive recursive functions. Electr. Notes Theor. Comput. Sci., 322:227-242, 2016. URL: http://dx.doi.org/10.1016/j.entcs.2016.03.016.
  15. K. S. Perumalla. Introduction to Reversible Computing. Chapman &Hall/CRC Computational Science. CRC Press, 2013. URL: http://dx.doi.org/10.1201/b15719.
  16. P. Selinger. A survey of graphical languages for monoidal categories. In B. Coecke, editor, New Structures for Physics, Lect. Notes in Physics, pages 289-355. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-12821-9_4.
  17. G. Winskel. The Formal Semantics of Programming Languages: An Introduction. MIT Press, 1993. Google Scholar
  18. Tetsuo Yokoyama. Reversible computation and reversible programming languages. Electr. Notes Theor. Comput. Sci., 253(6):71-81, 2010. URL: http://dx.doi.org/10.1016/j.entcs.2010.02.007.
  19. Tetsuo Yokoyama, Holger Bock Axelsen, and Robert Glück. Principles of a reversible programming language. In Alex Ramírez, Gianfranco Bilardi, and Michael Gschwind, editors, Proceedings of the 5th Conference on Computing Frontiers, 2008, Ischia, Italy, May 5-7, 2008, pages 43-54. ACM, 2008. URL: http://dx.doi.org/10.1145/1366230.1366239.
  20. Tetsuo Yokoyama and Robert Glück. A reversible programming language and its invertible self-interpreter. In G. Ramalingam and Eelco Visser, editors, Proceedings of the 2007 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2007, Nice, France, January 15-16, 2007, pages 144-153. ACM, 2007. URL: http://dx.doi.org/10.1145/1244381.1244404.
  21. M. Zorzi. On quantum lambda calculi: A foundational perspective. Math. Struct. Comput. Sci., 26(7):1107-1195, 2016. URL: http://dx.doi.org/10.1017/s0960129514000425.
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