DROPS

Document

DOI: 10.4230/LIPIcs.TYPES.2015.7

A Certified Study of a Reversible Programming Language

Authors: Luca Paolini, Mauro Piccolo, and Luca Roversi

Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{paolini_et_al:LIPIcs.TYPES.2015.7,
  author =	{Paolini, Luca and Piccolo, Mauro and Roversi, Luca},
  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 =	{Uustalu, Tarmo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.7},
  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}
}

Document

DOI: 10.4230/LIPIcs.TLCA.2015.211

Standardization of a Call-By-Value Lambda-Calculus

Authors: Giulio Guerrieri, Luca Paolini, and Simona Ronchi Della Rocca

Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)

Abstract

We study an extension of Plotkin's call-by-value lambda-calculus by means of two commutation rules (sigma-reductions). Recently, it has been proved that this extended calculus provides elegant characterizations of many semantic properties, as for example solvability. We prove a standardization theorem for this calculus by generalizing Takahashi's approach of parallel reductions. The standardization property allows us to prove that our calculus is conservative with respect to the Plotkin's one. In particular, we show that the notion of solvability for this calculus coincides with that for Plotkin's call-by-value lambda-calculus.

Cite as

Giulio Guerrieri, Luca Paolini, and Simona Ronchi Della Rocca. Standardization of a Call-By-Value Lambda-Calculus. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 211-225, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{guerrieri_et_al:LIPIcs.TLCA.2015.211,
  author =	{Guerrieri, Giulio and Paolini, Luca and Ronchi Della Rocca, Simona},
  title =	{{Standardization of a Call-By-Value Lambda-Calculus}},
  booktitle =	{13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
  pages =	{211--225},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-87-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{38},
  editor =	{Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.211},
  URN =		{urn:nbn:de:0030-drops-51655},
  doi =		{10.4230/LIPIcs.TLCA.2015.211},
  annote =	{Keywords: standardization,sequentialization,lambda-calculus,sigma-reduction,par- allel reduction, call-by-value, head reduction, internal reduction, solvability}
}

Search Results

Documents authored by Paolini, Luca

A Certified Study of a Reversible Programming Language

Abstract

Cite as

Standardization of a Call-By-Value Lambda-Calculus

Abstract

Cite as

Thanks for your feedback!

Could not send message