Download the complete article:

@inproceedings{paolini2018lipics,
  author = {Luca Paolini and Mauro Piccolo and Luca Roversi},
  issn = {1868-8969},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  editor = {Tarmo Uustalu},
  url = {http://drops.dagstuhl.de/opus/portals/lipics/index.php?semnr=16061},
  isbn = {978-3-95977-030-9},
  tag = {{LIPIcs}},
  localfile = {http://www.di.unito.it/~paolini/papers/2015types.pdf},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany},
  annote = {Keywords: reversible computing, Janus, operational semantics,
            bi-deterministic evaluation, categorical semantics},
  doi = {10.4230/LIPIcs.TYPES.2015.7},
  volume = 69,
  booktitle = {21st International Conference on Types for Proofs and Programs
               (TYPES 2015)},
  title = {{A Certified Study of a Reversible Programming Language}},
  abstract = {We advance in the study of the semantics of Janus, i.e.\ 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.},
  year = 2018,
  pages = {7:1--7:21},
}

This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)