A certified study of a reversible programming language

DOI10.4230/LIPICS.TYPES.2015.7MaRDI QIDQ4580228zbMATH OpenOpenAlexFDO

Authors Luca Paolini, Mauro Piccolo, Luca Roversi

Publication date 13 August 2018

Full work available at URL https://drops.dagstuhl.de/opus/volltexte/2018/8477/pdf/LIPIcs-TYPES-2015-7.pdf/

zbMATH Keywords

bi-deterministic evaluationcategorical semanticsJanusoperational semanticsreversible computing

Mathematics Subject Classification ID

Categorical semantics of formal languages (18C50) Theory of programming languages (68N15) Semantics in the theory of computing (68Q55) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Reversible Programs Have Reversible Semantics
• En garde! Unguarded iteration for reversible computation in the delay monad
• Towards a reversible functional language
• \(\mathsf{CoreFun}\): a typed functional reversible core language
• A categorical foundation for structured reversible flowchart languages: soundness and adequacy

Cites work

• A class of reversible primitive recursive functions
• A survey of graphical languages for monoidal categories
• scientific article; zbMATH DE number 439891 (Why is no real title available?)
• scientific article; zbMATH DE number 2134910 (Why is no real title available?)
• Isomorphic interpreters from logically reversible abstract machines
• Logical Reversibility of Computation
• On quantum lambda calculi: a foundational perspective
• Reversible Flowchart Languages and the Structured Reversible Program Theorem
• Reversible Machine Code and Its Abstract Processor Architecture
• Some Domain Theory and Denotational Semantics in Coq
• The Matita interactive theorem prover
• What do reversible programs compute?

Cited in

(8)

• Implementing reversible object-oriented language features on reversible machines
• The fixed point problem of a simple reversible language
• A class of recursive permutations which is primitive recursive complete
• Certifying algorithms and relevant properties of reversible primitive permutations with \textsf{Lean}
• From reversible programming languages to reversible metalanguages
• En garde! Unguarded iteration for reversible computation in the delay monad
• A type-assignment of linear erasure and duplication
• Reversible Programs Have Reversible Semantics

Describes a project that uses

Uses Software

• Matita
• Theseus

This page was built for publication: A certified study of a reversible programming language

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4580228)