A Certified Study of a Reversible Programming Language

DOI10.4230/LIPIcs.TYPES.2015.7zbMath1433.68080OpenAlexW2623394745MaRDI QIDQ4580228

Mauro Piccolo, Luca Paolini, 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

operational semanticscategorical semanticsreversible computingJanusbi-deterministic evaluation

Mathematics Subject Classification ID

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

Related Items (5)

From reversible programming languages to reversible metalanguages ⋮ A type-assignment of linear erasure and duplication ⋮ 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}

Uses Software

• Matita
• Theseus

Cites Work

• Unnamed Item
• Unnamed Item
• A class of reversible primitive recursive functions
• On quantum lambda calculi: a foundational perspective
• What Do Reversible Programs Compute?
• A Survey of Graphical Languages for Monoidal Categories
• Some Domain Theory and Denotational Semantics in Coq
• Isomorphic Interpreters from Logically Reversible Abstract Machines
• Reversible Machine Code and Its Abstract Processor Architecture
• Reversible Flowchart Languages and the Structured Reversible Program Theorem
• The Matita Interactive Theorem Prover
• Logical Reversibility of Computation

This page was built for publication: A Certified Study of a Reversible Programming Language