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

categorical semanticsreversible computingoperational semanticsJanusbi-deterministic evaluation

Mathematics Subject Classification ID

Theory of programming languages (68N15) Categorical semantics of formal languages (18C50) 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

• scientific article; zbMATH DE number 439891 (Why is no real title available?)
• scientific article; zbMATH DE number 2134910 (Why is no real title available?)
• A class of reversible primitive recursive functions
• A survey of graphical languages for monoidal categories
• 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)

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

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)