# Carlos Olarte

I'm professor at ECT UFRN, Natal (Brazil) and CNPq Researcher (**Bolsista de Produtividade em Pesquisa do CNPq **2019-2021).

My research interests are logic, formal methods and concurrency theory.

I'm also member of the AVISPA research group.

Here my CV in PDF and CNPq-lattes.

email: carlos.olarte *at* gmail.com

## Publications

Publications

My list of publications is available in DBLP and ORCID. Some pre-printed version are available here.

## Drafts

Drafts

**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

Recently Accepted Papers

**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.- Verification techniques for a network algebra (with L. Brodo).
*Fundamenta Informaticae**.*(PDF). Companion tool SiLVer. - Dynamic slicing for Concurrent Constraint Languages (with M. Falaschi, M. Gabbrielli and C. Palamidessi).
*Fundamenta Informaticae**.*(PDF, to appear in 2020). - Hybrid linear logic, revisited (with K. Chaudhuri, J. Despeyroux and E. Pimentel). Mathematical Structures in Computer Science. (HAL version).

## Tools

Tools

- A Focused Linear Logical Framework and its Application to Metatheory of Object Logics.
- Benchmarks for intuitionistic linear logic and provers.
- Structural Proof Theory in Maude (WRLA'18 paper).
- Formalizing (First Order) Linear Logic (cut-elimination + focusing) in Coq.
- Prover for Simply Dependent Multimodal Linear Systems.
- SiLVer: Symbolic links verifier. A web interface is available here.
- Prover for Full Lambek Calculus with Weakening and Bounded Contraction.
- Slicer for CCP (LOPSTR'16 paper).
- ESTRO: From Multiparty Session Types to Event-B
- LolliP: Linear CCP interpreter
- Alcove: Access Permissions Linear COnstraints VErifier

## Projects

Projects

- 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.*

## PC Committees

PC Committees

- 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.