My research interests are logic, formal methods and concurrency theory.
I'm also member of the AVISPA research group.
email: carlos.olarte at gmail.com
A subexponential view of domains in session types (with Daniele Nantes and Daniel Ventura). Linear logic (LL) has inspired the design of many computational systems, offering reasoning techniques built on top of its meta-theory. Since its inception, several connections between concurrent systems and LL have emerged from different perspectives. In the last decade, the seminal work of Caires and Pfenning showed that formulas in LL can be interpreted as session types and processes in the pi-calculus as proof terms. This leads to a Curry-Howard interpretation where proof reductions in the cut-elimination procedure correspond to process reductions/interactions. The subexponentials in LL have also played an important role in concurrent systems since they can be interpreted in different ways, including timed, spatial and even epistemic modalities in distributed systems. In this paper we address the question: What is the meaning of the subexponentials from the point of view of a session type interpretation? Our answer is a pi-like process calculus where agents reside in locations/sites and they make it explicit how the communication among the different sites should happen. The design of this language relies completely on the proof theory of the subexponentials in LL, thus extending the Caires-Pfenning interpretation in an elegant way. Submitted to LSFA'21 (PDF).
A Rewriting Logic Approach to Specification, Proof-search, and Meta-proofs in Sequent Systems (with Elaine Pimentel and Camilo Rocha): This paper develops an algorithmic-based approach for proving inductive properties of propositional sequent systems such as admissibility, invertibility, cut-elimination, and identity expansion. Although undecidable in general, these structural properties are crucial in proof theory because they can reduce the proof-search effort and further be used as scaffolding for obtaining other meta-results such as consistency. The algorithms -- which take advantage of the rewriting logic meta-logical framework, and use rewrite- and narrowing-based reasoning -- are explained in detail and illustrated with examples throughout the paper. They have been fully mechanized in the L-Framework, thus offering both a formal specification language and off-the-shelf mechanization of the proof-search algorithms coming together with semi-decision procedures for proving theorems and meta-theorems of the object system. As illustrated with case studies in the paper, the L-Framework, achieves a great degree of automation when used on several propositional sequent systems, including single conclusion and multi-conclusion intuitionistic logic, classical logic, classical linear logic and its dyadic system, intuitionistic linear logic, and normal modal logics. (arXiv, code).
A Focused Linear Logical Framework and its Application to Meta Theory of Object Logics (with Amy Felty and Bruno Xavier): We have formalized the proof of cut-elimination for first-order focused linear logic (LL) directly in the focused system. We have also encoded the inference rules of other logics as LL theories and formalized the necessary conditions for those logics to have the cut-elimination property. We then obtained, for free, cut-elimination for propositional classical, minimal and intuitionistic logics. We have also used the LL meta-theory to formalize the relative completeness of natural deduction and sequent calculus in first-order minimal logic. The formalization is here and the draft of the paper here. Submitted to MSCS.
Recently Accepted Papers
Process-As-Formula Interpretation: A Substructural Multimodal View (with Elaine Pimentel and Vivek Nigam): In this survey, we show how the processes-as-formulas interpretation, where computations and proof-search are strongly connected, can be used to specify different concurrent behaviors as logical theories. The proposed interpretation is parametric and modular, and it faithfully captures behaviors such as: Linear and spatial computations, epistemic state of agents, and preferences in concurrent systems. The key for this modularity is the incorporation of multimodalities in a resource aware logic, together with the ability of quantifying on such modalities. We achieve tight adequacy theorems by relying on a focusing discipline that allows for controlling the proof search process. (Invited talk at FSCD'21).
A Semantic Framework for PEGs (with Sérgio Medeiros): Parsing Expression Grammars (PEGs) are a recognition-based formalism which allows to describe the syntactical and the lexical elements of a language. The main difference between Context-Free Grammars (CFGs) and PEGs relies on the interpretation of the choice operator: while the CFGs’ unordered choice e ∣ e′ is interpreted as the union of the languages recognized by e and e′, the PEGs’ prioritized choice e e′ discards e′ if e succeeds. Such subtle, but important difference, changes the language recognized and yields more efficient parsing algorithms. This paper proposes a rewriting logic semantics for PEGs. We start with a rewrite theory giving meaning to the usual constructs in PEGs. Later, we show that cuts, a mechanism for controlling backtracks in PEGs, finds also a natural representation in our framework. We generalize such mechanism, allowing for both local and global cuts with a precise, unified and formal semantics. Hence, our work strives at better understanding and controlling backtracks in parsers for PEGs. The semantics we propose is executable and, besides being a parser with modest efficiency, it can be used as a playground to test different optimization ideas. More importantly, it is a mathematical tool that can be used for different analyses. To appear in SLE 2020. (PDF).
A fresh view of linear logic as a logical framework (with Elaine Pimentel and Bruno Xavier): We use a linear-nested sequent (LNS) presentation of SLL (a variant of linear logic with subexponentials) and show that it is possible to establish a cut-elimination criterion for LNS proof systems for K, 4, KT, KD, S4 and the multi-conclusion LNS system for intuitionistic logic (mLJ). The sufficient conditions for cut-elimination are easy to verify. We thus contribute with procedures for checking cut-elimination of several logical systems that are widely used in philosophy, mathematics and computer science. The paper is here. Submitted to LSFA'20.
A constraint-based language for multiparty interactions (with Linda Brodo): We extend the the Core Network Algebra (CNA) with constraints that declaratively allow the modeler to restrict the interaction that should actually happen. Our extended process algebra, called CCNA, finds application in balancing the interactions in a concurrent system, leading to a simple, deadlock-free and fair solution for the Dinning Philosopher problem. Our definition of constraints is general enough and it offers the possibility of accumulating costs in a multiparty negotiation. Hence, only computations respecting the thresholds imposed by the modeler are observed. We use this machinery to neatly model a Service Level Agreement protocol. We develop the theory of CCNA including its operational semantics and a behavioral equivalence that we prove to be a congruence. We also propose a prototypical implementation that allows us to verify, automatically, some of the systems explored in the paper. Submitted to LSFA'20.
RESPEG: Rewriting Semantics for PEGs (SLE'20 paper).
L-Framework: structural proof theory in Maude (WRLA'18 paper).
Slicer for CCP (FI'20 paper).
ESTRO: From Multiparty Session Types to Event-B (SAC'16 paper)
LolliP: Linear CCP interpreter
Alcove: Access Permissions Linear COnstraints VErifier (TPLP'18 paper).
CNPq Bolsa de Produtividade (2019-2022): LOGOCOSMICS: LOgica, joGOs e Cálculos de prOcessos para Sistemas ModaIs ConcorrenteS
CNPq Projeto Universal (2019-2022): Sistemas concorrentes: semântica, provas e modelos declarativos.
EPIC: EPistemic Interactive Concurrency. STIC-AmSud Project. In collaboration with INRIA and Universidad Javeriana Cali. 2017.
MOSAIC - Modalities in Substructural Logics: Theory, Methods and Applications. Sklodowska-Curie Action: RISE Grant Agreement no 101007627.
International Conference on Software Language Engineering SLE'2021.
International Conference on Logic Programming ICLP'2021.
Co-chair of WBL'21 (Workshop Brasileiro de Lógica).
16th International Workshop on Logical and Semantic Frameworks, with Applications. LSFA'21.
15th International Workshop on Logical and Semantic Frameworks, with Applications. LSFA'20.
Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2020.
35th International Conference on Logic Programming ICLP'19.
27th International Conference on Automated Deduction CADE'27.
29th International Symposium on Logic-Based Program Synthesis and Transformation LOPSTR'19.
Sixth Workshop on Proof eXchange for Theorem Proving PxTP 2019.
I'm co-chair of LSFA'18.
Logical Frameworks and Meta-Languages: Theory and Practice - LFMTP'18.
5th Workshop on Horn Clauses for Verification and Synthesis - HCVS'18.