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

DOI10.1016/j.jlamp.2023.100923OpenAlexW4387873252MaRDI QIDQ6151610

Luca Roversi, Giacomo Maletto

Publication date: 12 February 2024

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

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

zbMATH Keywords

primitive recursionreversible computationLean

Mathematics Subject Classification ID

Computer science (68-XX)

Cites Work

• Unnamed Item
• Unnamed Item
• Generation of invertible functions
• Linear programs in a simple reversible language.
• Theory of reversible computing
• The fixed point problem of a simple reversible language
• A class of recursive permutations which is primitive recursive complete
• On the expressivity of total reversible programming languages
• Certifying algorithms and relevant properties of reversible primitive permutations with \textsf{Lean}
• User interaction with the Matita proof assistant
• Reversible Computing
• The Lean Theorem Prover (System Description)
• Irreversibility and Heat Generation in the Computing Process

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