Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Paolini, Luca; Piccolo, Mauro; Roversi, Luca http://www.dagstuhl.de/lipics License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-84771
URL:

; ;

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: 2018


DROPS-Home | Fulltext Search | Imprint Published by LZI