This Ph.D. thesis addresses the problem of giving computational interpretation to proofs in classical logic. As such, it presents three calculi reflecting different approaches in the study of this area. The thesis consists of three parts. The first part introduces the *X calculus, whose terms represent proofs in the classical sequent calculus, and whose reduction rules capture most of the features of cut-elimination in sequent calculus. This calculus introduces terms which enable explicit imp...
We present a calculus providing a Curry-Howard correspondence to classical logic represented in the sequent calculus with explicit structural rules, namely weakening and contraction. These structural rules introduce explicit erasure and duplication of terms, respectively. We present a type system for which we prove the type-preservation under reduction. A mutual relation with classical calculus featuring implicit structural rules has been studied in detail. From this analysis we derive strong...
In this paper we consider two-opinion voter models on dynamic random graphs,in which the joint dynamics of opinions and graphs acts as one-way feedback,i.e., edges appear and disappear over time depending on the opinions of the twoconnected vertices, while the opinion dynamics does not depend on the edgeprocess. Our goal is to investigate the joint evolution of the entries of avoter subgraph count vector, i.e., vector of subgraphs where each vertex has aspecific opinion, in the regime that th...
The present overview and gentle introduction to Grassmannian calculus andsome of its applications to probability collects the notes of a mini-coursegiven by the authors at the Brazilian School of Probability, August 5-9, 2024,in Salvador, Bahia, Brazil. The content is by no means comprehensive, and is apersonal summary and interpretation of results and applications of thisinteresting area of research.