7 citations · 28 across the 17 of their papers we have counts for
15 papers · 1 filter
Certifying algorithms and relevant properties of Reversible Primitive Permutations with Lean
Giacomo Maletto, Luca Roversi
Reversible Primitive Permutations (RPP) are recursively defined functions designed to model Reversible Computation. We illustrate a proof, fully developed with the proof-assistant…
Probabilistic Soft Type Assignment
Gianluca Curzi, Luca Roversi
We model randomized complexity classes in the style of Implicit Computational Complexity. We introduce PSTA, a probabilistic version of STA, the type-theoretical counterpart of Sof…
A type-assignment of linear erasure and duplication
Gianluca Curzi, Luca Roversi
We introduce , a type-assignment system for the linear -calculus that extends second-order , i.e., intuitionistic multiplicative Linear Logic, by…
Subatomic systems need not be subatomic
Luca Roversi
Subatomic systems were recently introduced to identify the structural principles underpinning the normalization of proofs. "Subatomic" means that we can reformulate logical systems…
Quantum Programming Made Easy
Luca Paolini, Luca Roversi, Margherita Zorzi
We present IQu, namely a quantum programming language that extends Reynold's Idealized Algol, the paradigmatic core of Algol-like languages. IQu combines imperative programming wit…
Communication, and concurrency with logic-based restriction inside a calculus of structures
Luca Roversi
It is well known that we can use structural proof theory to refine, or generalize, existing paradigmatic computational primitives, or to discover new ones. Under such a point of vi…