Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2015.7
URN: urn:nbn:de:0030-drops-84771
URL: https://drops.dagstuhl.de/opus/volltexte/2018/8477/
Paolini, Luca ; Piccolo, Mauro ; Roversi, Luca
A Certified Study of a Reversible Programming Language
| pdf-format: |
|
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.
BibTeX - Entry
@InProceedings{paolini_et_al:LIPIcs:2018:8477,
author = {Luca Paolini and Mauro Piccolo and Luca Roversi},
title = {{A Certified Study of a Reversible Programming Language}},
booktitle = {21st International Conference on Types for Proofs and Programs (TYPES 2015)},
pages = {7:1--7:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-030-9},
ISSN = {1868-8969},
year = {2018},
volume = {69},
editor = {Tarmo Uustalu},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2018/8477},
URN = {urn:nbn:de:0030-drops-84771},
doi = {10.4230/LIPIcs.TYPES.2015.7},
annote = {Keywords: reversible computing, Janus, operational semantics, bi-deterministic evaluation, categorical semantics}
}
| Keywords: | reversible computing, Janus, operational semantics, bi-deterministic evaluation, categorical semantics | |
| Seminar: | 21st International Conference on Types for Proofs and Programs (TYPES 2015) | |
| Issue date: | 2018 | |
| Date of publication: | 15.03.2018 |
