BZPEERReading, trust and collaboration for research
Menu

Discover

GraphFollow connections around a paper, topic or saved view.

Workspaces

HomePick up where your research flow left off.InboxHandle requests, replies and notifications from one place.CollectionsCurate reading lists, evidence sets and shareable dossiers.ResearchSee your private provenance graph, trail and imports.CollaborationMove from discovery into focused discussion rooms.PublishDraft, preview and publish full-text research articles.

Network

ExpertsFind specialists worth following or asking for help.CommunitiesJoin research circles organized around shared work.PartnersSee external organizations active around the same topics.

Opportunities

ListingsBrowse roles, calls and collaborations with clearer fit signals.

Account

Log inReturn to your reading and collaboration workspace.Create accountStart saving work, following people and joining teams.
Log inCreate account

Researcher profile

Stefano Berardi

Stefano Berardi contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate
Logic in Computer Sciencemath.LOmath.CT

Trust snapshot

Quick read

Trust 21 - EmergingVerification L1Unclaimed author
9works
0followers
3topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

9 published item(s)

preprint2024arXiv

Termination of Rewriting on Reversible Boolean Circuits as a Free 3-Category Problem

Reversible Boolean Circuits are an interesting computational model under many aspects and in different fields, ranging from Reversible Computing to Quantum Computing. Our contribution is to describe a specific class of Reversible Boolean Circuits - which is as expressive as classical circuits - as a bi-dimensional diagrammatic programming language. We uniformly represent the Reversible Boolean Circuits we focus on as a free 3-category Toff. This formalism allows us to incorporate the representation of circuits and of rewriting rules on them, and to prove termination of rewriting. Termination follows from defining a non-identities-preserving functor from our free 3-category Toff into a suitable 3-category Move that traces the "moves" applied to wires inside circuits.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Ramsey's Theorem for Pairs and $k$ Colors as a Sub-Classical Principle of Arithmetic

The purpose is to study the strength of Ramsey&#39;s Theorem for pairs restricted to recursive assignments of $k$-many colors, with respect to Intuitionistic Heyting Arithmetic. We prove that for every natural number $k \geq 2$, Ramsey&#39;s Theorem for pairs and recursive assignments of $k$ colors is equivalent to the Limited Lesser Principle of Omniscience for $Σ^0_3$ formulas over Heyting Arithmetic. Alternatively, the same theorem over intuitionistic arithmetic is equivalent to: for every recursively enumerable infinite $k$-ary tree there is some $i < k$ and some branch with infinitely many children of index $i$.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

An intuitionistic version of Ramsey Theorem (italian version)

Ramsey Theorem [6] for pairs is intuitionistically but not classically provable: it is equivalent to a subclassical principle [2]. In this note we show that Ramsey may be restated in an intuitionistically provable form, which is informative (or at least without negations), and classically equivalent to the original. With respect to previous works of the same kind, we do not use no counterexample as in [1], [5], nor we add a new principle to the intuitionism as in [4]. We claim that this intuitionistic version of Ramsey could be use to replace Ramsey Theorem in the convergence proof of programs included in [3]. [1] Gianluigi Bellin. Ramsey interpreted: a parametric version of Ramsey Theorem. In AMS, editor, Logic and Computation: Proceedings of a Symposium held at Carnegie Mellon University, volume 106. [2] Stefano Berardi, Silvia Steila, Ramsey Theorem for pairs as a classical principle in Intuitionistic Arithmetic, Submitted to the proceedings of Types 2013 in Toulouse. [3] Byron Cook, Abigail See, Florian Zuleger, Ramsey vs. Lexicographic Termination Proving, LNCS 7795, 2013, Springer Berlin Heidelberg. [4] Thierry Coquand. A direct proof of Ramsey Theorem. [5] Paulo Oliva and Thomas Powell. A Constructive Interpretation of Ramsey Theorem via the Product of Selection Functions. CoRR, arXiv:1204.5631, 2012. [6] F. P. Ramsey. On a problem in formal logic. Proc. London Math. Soc., 1930.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Knowledge Spaces and the Completeness of Learning Strategies

We propose a theory of learning aimed to formalize some ideas underlying Coquand&#39;s game semantics and Krivine&#39;s realizability of classical logic. We introduce a notion of knowledge state together with a new topology, capturing finite positive and negative information that guides a learning strategy. We use a leading example to illustrate how non-constructive proofs lead to continuous and effective learning strategies over knowledge spaces, and prove that our learning semantics is sound and complete w.r.t. classical truth, as it is the case for Coquand&#39;s and Krivine&#39;s approaches.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Proving termination with transition invariants of height omega

The Termination Theorem by Podelski and Rybalchenko states that the reduction relations which are terminating from any initial state are exactly the reduction relations whose transitive closure, restricted to the accessible states, is included in some finite union of well-founded relations. An alternative statement of the theorem is that terminating reduction relations are precisely those having a &#34;disjunctively well-founded transition invariant&#34;. From this result the same authors and Byron Cook designed an algorithm checking a sufficient condition for termination for a while-if program. The algorithm looks for a disjunctively well-founded transition invariant, made of well-founded relations of height omega, and if it finds it, it deduces the termination for the while-if program using the Termination Theorem. This raises an interesting question: What is the status of reduction relations having a disjunctively well-founded transition invariant where each relation has height omega? An answer to this question can lead to a characterization of the set of while-if programs which the termination algorithm can prove to be terminating. The goal of this work is to prove that they are exactly the set of reduction relations having height omega^n for some n < omega. Besides, if all the relations in the transition invariant are primitive recursive and the reduction relation is the graph of the restriction to some primitive recursive set of a primitive recursive map, then a final state is computable by some primitive recursive map in the initial state. As a corollary we derive that the set of functions, having at least one implementation in Podelski Rybalchenko while-if language with a well-founded disjunctively transition invariant where each relation has height omega, is exactly the set of primitive recursive functions.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Non-monotonic Pre-fixed Points and Learning

We consider the problem of finding pre-fixed points of interactive realizers over arbitrary knowledge spaces, obtaining a relative recursive procedure. Knowledge spaces and interactive realizers are an abstract setting to represent learning processes, that can interpret non-constructive proofs. Atomic pieces of information of a knowledge space are stratified into levels, and evaluated into truth values depending on knowledge states. Realizers are then used to define operators that extend a given state by adding and possibly removing atoms: in a learning process states of knowledge change nonmonotonically. Existence of a pre-fixed point of a realizer is equivalent to the termination of the learning process with some state of knowledge which is free of patent contradictions and such that there is nothing to add. In this paper we generalize our previous results in the case of level 2 knowledge spaces and deterministic operators to the case of omega-level knowledge spaces and of non-deterministic operators.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

Proceedings Third International Workshop on Classical Logic and Computation

The fact that classical mathematical proofs of simply existential statements can be read as programs was established by Goedel and Kreisel half a century ago. But the possibility of extracting useful computational content from classical proofs was taken seriously only from the 1990s on when it was discovered that proof interpretations based on Goedel&#39;s and Kreisel&#39;s ideas can provide new nontrivial algorithms and numerical results, and the Curry-Howard correspondence can be extended to classical logic via programming concepts such as continuations and control operators. The workshop series &#34;Classical Logic and Computation&#34; aims to support a fruitful exchange of ideas between the various lines of research on computational aspects of classical logic. This volume contains the abstracts of the invited lectures and the accepted contributed papers of the third CL&C workshop which was held jointly with the workshop &#34;Program Extraction and Constructive Mathematics&#34; at the University of Brno in August 21-22, 2010, as a satellite of CSL and MFCS. The workshops were held in honour of Helmut Schwichtenberg who became &#34;professor emeritus&#34; in September 2010. The topics of the papers include the foundations, optimizations and applications of proof interpretations such as Hilbert&#39;s epsilon substitution method, Goedel&#39;s functional interpretation, learning based realizability and negative translations as well as special calculi and theories capturing computational and complexity-theoretic aspects of classical logic such as the lambda-mu-calculus, applicative theories, sequent-calculi, resolution and cut-elimination

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

Interactive Learning-Based Realizability for Heyting Arithmetic with EM1

We apply to the semantics of Arithmetic the idea of ``finite approximation&#39;&#39; used to provide computational interpretations of Herbrand&#39;s Theorem, and we interpret classical proofs as constructive proofs (with constructive rules for $\vee, \exists$) over a suitable structure $\StructureN$ for the language of natural numbers and maps of Gödel&#39;s system $\SystemT$. We introduce a new Realizability semantics we call ``Interactive learning-based Realizability&#39;&#39;, for Heyting Arithmetic plus $\EM_1$ (Excluded middle axiom restricted to $Σ^0_1$ formulas). Individuals of $\StructureN$ evolve with time, and realizers may ``interact&#39;&#39; with them, by influencing their evolution. We build our semantics over Avigad&#39;s fixed point result, but the same semantics may be defined over different constructive interpretations of classical arithmetic (Berardi and de&#39; Liguoro use continuations). Our notion of realizability extends intuitionistic realizability and differs from it only in the atomic case: we interpret atomic realizers as ``learning agents&#39;&#39;.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

Interactive Realizers and Monads

We propose a realizability interpretation of a system for quantifier free arithmetic which is equivalent to the fragment of classical arithmetic without &#34;nested&#34; quantifiers, called here EM1-arithmetic. We interpret classical proofs as interactive learning strategies, namely as processes going through several stages of knowledge and learning by interacting with the &#34;environment&#34; and with each other. We give a categorical presentation of the interpretation through the construction of two suitable monads.

0 citations0 reviewsNo code linkedOpen access