Certifying algorithms and relevant properties of reversible primitive permutations with \textsf{Lean}

DOI10.1007/978-3-031-09005-9_8OpenAlexW4221143021MaRDI QIDQ2097420

Luca Roversi, Giacomo Maletto

Publication date: 11 November 2022

Full work available at URL: https://arxiv.org/abs/2201.10443

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Quantum computation (81P68) Other nonclassical models of computation (68Q09)

Related Items (1)

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

Uses Software

• Matita
• Lean
• GitHub

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
• The Lean 4 theorem prover and programming language
• User interaction with the Matita proof assistant
• Reversible Computing
• The Lean Theorem Prover (System Description)
• A Certified Study of a Reversible Programming Language

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