Certifying expressive power and algorithms of reversible primitive permutations with \textsf{Lean}

DOI10.1016/J.JLAMP.2023.100923MaRDI QIDQ6151610zbMATH OpenOpenAlexFDO

Authors Giacomo Maletto, Luca Roversi

Publication date 12 February 2024

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1016/j.jlamp.2023.100923

zbMATH Keywords

Leanprimitive recursionreversible computation

Mathematics Subject Classification ID

Computer science (68-XX)

Cites work

• A class of recursive permutations which is primitive recursive complete
• Certifying algorithms and relevant properties of reversible primitive permutations with \textsf{Lean}
• Generation of invertible functions
• scientific article; zbMATH DE number 3291134 (Why is no real title available?)
• scientific article; zbMATH DE number 7649961 (Why is no real title available?)
• Irreversibility and Heat Generation in the Computing Process
• Linear programs in a simple reversible language.
• On the expressivity of total reversible programming languages
• Reversible Computing
• The fixed point problem of a simple reversible language
• The Lean theorem prover (system description)
• Theory of reversible computing
• User interaction with the Matita proof assistant

Cited in

(1)

• Algorithmically expressive, always-terminating model for reversible computation

This page was built for publication: Certifying expressive power and algorithms of reversible primitive permutations with \textsf{Lean}

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