Carlos Olarte

I'm professor at ECT UFRN, Natal (Brazil) and  CNPq Researcher (Bolsista de Produtividade em Pesquisa do CNPq - Nível 2, Ciências da Computação 2016-2019).
My research interests are logic, formal methods, concurrency theory and concurrent constraint programming. 

I'm also member of the AVISPA research group.
Here my CV in PDF and CNPq-lattes.

email: carlos.olarte at 


  • EPIC: EPistemic Interactive Concurrency. STIC-AmSud Project. In collaboration with INRIA and Universidad Javeriana Cali. 2017.
  • CNPq Bolsa de Produtividade (2016-2019): Modalidades em Concorrência: Fundamentos e aplicações em Bio-informática e Computação Orientada a Serviços
  • MUSICAL: Music and spatial interaction with constraints, algebra and logic: foundations and applications.

PC Committees 
  • 27th International Conference on Automated Deduction CADE'27.
  • 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.
  • 2nd Brazilian School on Formal Methods and Computational Theory - ETMF2017.
  • Recent Advances in Concurrency and Logic - RADICAL'17.
  • Dynamic Logic: new trends and applications DaLi17.
  • I Workshop Escola de Inverno em Teoria da Computação WEITC2017.
  • Escola de Informática Teórica e Métodos Formais ETFM'16.
  • Logic-Based Program Synthesis and Transformation, LOPSTR 2015.
  • CSP track of SAC 2015
    • A Logical Framework for Modelling Breast Cancer Progression (with Joelle Despeyroux, Amy Felty and Pietro Lio).  Proof in Coq are available here
    • Verification techniques for a network algebra (with Linda Brodo). Submitted to Fundamenta Informaticae. (PDF). Companion tool SiLVer 
    • Hybrid Linear Logic, revisited (with Kaustuv Chaudhuri, Joelle Despeyroux and Elaine Pimentel). Submitted to MSCS (PDF). 
    Recently Accepted Papers 
    • An Assertion language for slicing Constraint Logic Languages (with Moreno Falaschi). To appear in LOPSTR'18 (arXiv version). Companion tool.  
    • The ILLTP Library for Intuitionistic Linear Logic (with Valeria de Paiva, Elaine Pimentel and Giselle Reis) (PDF). To appear in Proc. of Linearity & TLLA.  The prover is available here and the benchmarks here.
    • Proving Structural Properties of Sequent Systems in Rewriting Logic (with Elaine Pimentel and Camilo Rocha) (PDF). To appear in Proceedings of WRLA'18. Companion tool here.  
    • A Concurrent Constraint Programming Interpretation of Access Permissions (with Elaine Pimentel and Camilo Rueda). In TPLP (18). (arXiv version).
    • Mechanizing Linear Logic in Coq (with Bruno Xavier, Giselle Reis and Vivek Nigam). To appear in Proc. of  LSFA'17 (PDF). Proofs in Coq are  here
    • On subexponentials, focusing and modalities in concurrent systems (with Vivek Nigam and Elaine Pimentel) in Theoretical Computer Sciece (693). 
    • On concurrent behaviors and focusing in linear logic (with Elaine Pimentel). Theoretical Computer Science (685). (Technical Report version). 
    • A unified view of modal and substructural logics (with Elaine Pimentel and Björn Lellmann).  In LPAR-21 (2017) (PDF). The implementation of the system can be found here.
    Subpages (1): Publications