43 citations · 72 across the 14 of their papers we have counts for
13 papers · 1 filter
Termination of Rewriting on Reversible Boolean Circuits as a Free 3-Category Problem
Adriano Barile, Stefano Berardi, Luca Roversi
Reversible Boolean Circuits are an interesting computational model under many aspects and in different fields, ranging from Reversible Computing to Quantum Computing. Our contribut…
Proceedings Seventh International Workshop on Classical Logic and Computation
Stefano Berardi, Alexandre Miquel
This special issue cover the seventh and last conference of the CL&C series, started in 2006 in San Servolo. Topics are the computational content of logics between intuitionistic l…
Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic
Stefano Berardi, Makoto Tatsuta
A cyclic proof system gives us another way of representing inductive definitions and efficient proof search. In 2011 Brotherston and Simpson conjectured the equivalence between the…
Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs
Stefano Berardi, Makoto Tatsuta
A cyclic proof system, called CLKID-omega, gives us another way of representing inductive definitions and efficient proof search. The 2005 paper by Brotherston showed that the prov…
A Sound, Complete and Effective Second Order Game Semantics
Stefano Berardi
We define a game semantics for second order classical arithmetic PA2 (with quantifiers over predicates on integers and full comprehension axiom). Our semantics is effective: moves…
Proceedings Sixth International Workshop on Classical Logic and Computation
Ulrich Kohlenbach, Steffen van Bakel, Stefano Berardi
The workshop series intends to cover research that investigates the computational aspects of classical logic and mathematics. Its focus is on unwinding the computational content of…