Skip to Main Content (Press Enter)

Logo UNITO
  • ×
  • Home
  • Pubblicazioni
  • Progetti
  • Persone
  • Competenze
  • Settori
  • Strutture
  • Terza Missione

UNI-FIND
Logo UNITO

|

UNI-FIND

unito.it
  • ×
  • Home
  • Pubblicazioni
  • Progetti
  • Persone
  • Competenze
  • Settori
  • Strutture
  • Terza Missione
  1. Pubblicazioni

Certifying Algorithms and Relevant Properties of Reversible Primitive Permutations with Lean

Contributo in Atti di convegno
Data di Pubblicazione:
2022
Abstract:
Reversible Primitive Permutations (RPP) are recursively defined functions designed to model Reversible Computation. We illustrate a proof, fully developed with the proof-assistant Lean, certifying that: ``RPP can encode every Primitive Recursive Function''. Our reworking of the original proof of that statement is conceptually simpler, fixes some bugs, suggests a new more primitive reversible iteration scheme for RPP, and, in order to keep formalization and semi-automatic proofs simple, led us to identify a single pattern that can generate some useful reversible algorithms in RPP: Cantor Pairing, Quotient/Reminder of integer division, truncated Square Root. Our Lean source code is available for experiments on Reversible Computation whose properties can be certified.
Tipologia CRIS:
04A-Conference paper in volume
Keywords:
Reversible computation, Reversible Primitive Permutations, Software Certification, PRF-Completeness, Lean Theorem Prover
Elenco autori:
Giacomo Maletto; Luca Roversi
Autori di Ateneo:
ROVERSI Luca
Link alla scheda completa:
https://iris.unito.it/handle/2318/1867901
Link al Full Text:
https://iris.unito.it/retrieve/handle/2318/1867901/1013804/220629-arxive-definitivo.pdf
Titolo del libro:
REVERSIBLE COMPUTATION - 14th International Conference RC2022 - Proceedings
Pubblicato in:
LECTURE NOTES IN COMPUTER SCIENCE
Journal
LECTURE NOTES IN COMPUTER SCIENCE
Series
  • Dati Generali
  • Aree Di Ricerca

Dati Generali

URL

https://arxiv.org/abs/2201.10443; https://link.springer.com/chapter/10.1007/978-3-031-09005-9_8

Aree Di Ricerca

Settori (5)


PE6_4 - Theoretical computer science, formal methods, automata - (2024)

CIBO, AGRICOLTURA e ALLEVAMENTI - Farmacologia Veterinaria

INFORMATICA, AUTOMAZIONE e INTELLIGENZA ARTIFICIALE - Industria X.0

PIANETA TERRA, AMBIENTE, CLIMA, ENERGIA e SOSTENIBILITA' - Diritto dell'Ambiente

PIANETA TERRA, AMBIENTE, CLIMA, ENERGIA e SOSTENIBILITA' - Informatica e Ambiente
  • Utilizzo dei cookie

Realizzato con VIVO | Designed by Cineca | 25.6.1.0