Theory of Computation

Session Types for Message-Passing Concurrency

Prof. Jorge A. Pérez (UGroningen)

Abstract.  Writing concurrent programs is notoriously difficult. In programs that communicate by exchanging messages over channels, one of the main

challenges is ensuring that the sequences of sent and received messages follow a well-defined protocol. Session types address this challenge by providing abstract specifications of channel-based communication protocols. They enable static verification of communication correctness: well-typed programs are guaranteed to respect their intended protocols, avoiding both communication mismatches and deadlocks.

This presentation involves two parts. In the first one, I will provide a general introduction to correctness in message-passing concurrency and to protocol specification using session types. In the second part, I will focus on the interplay of session types and asynchronous communication. I will overview recent work on ensuring the deadlock-freedom property for message-passing processes that communicate asynchronously in cyclic process networks governed by session types. To this end, I will offer a gradual presentation of three typed process frameworks and outline how they provide different levels of deadlock-freedom guarantees.

Truth-tables for Intuitionistic Propositional Logic

Prof. Bruno Lopes (UFF)

Abstract. Kurt Gödel proved that it is not possible to characterize intuitionistic propositional logic (𝐼𝑃𝐿) by means of finite and deterministic truth-tables. After extending the same result with respect to non-deterministic matrices (Nmatrices), we provide a semantical characterization of  𝐼𝑃𝐿 by means of a  3-valued Nmatrix with a restricted set of valuations. This structure allows to define an algorithm to delete unsound rows from the non-deterministic truth-tables generated for each formula, which constitutes a new and very simple decision procedure for  𝐼𝑃𝐿. This method can be seen as truth-tables in a broader sense, and a way to overcome Gödel’s limiting result.

A Typed Semantics for Parsing and its Applications

Prof. Rodrigo Ribeiro (UFOP)

Abstract. While parsing is a foundational problem in computer science, it remains an active area of research with significant open challenges, including formal verification, handling of complex data formats, and the development of new formalisms for dealing with extensible languages.

We show how ideas from type theory can be used together with parsing expression grammars to provide solutions to these problem

Lean 4 na Indústria: Da Teoria à Prática em Sistemas Criptográficos e Zero-Knowledge

Fabrício Paranhos (Nethermind)

Resumo. Esta palestra apresenta a experiência prática da equipe Lamport (Nethermind) na aplicação de verificação formal com Lean 4 em sistemas criptográficos de produção. Exploraremos como Lean 4 transcende seu uso tradicional na formalização matemática para se tornar uma ferramenta essencial na verificação de sistemas críticos de zero-knowledge, incluindo a verificação formal de sistemas de restrições, máquinas virtuais ZK, e protocolos criptográficos complexos.

Compartilharemos casos concretos do desenvolvimento de modelos formais da EVM e Yul em Lean 4, discutindo os desafios únicos de traduzir requisitos industriais em especificações formais verificáveis. Abordaremos também a verificação de algoritmos criptográficos e protocolos distribuídos para contratos inteligentes, destacando como as capacidades de metaprogramação e o sistema de tipos dependentes do Lean 4 permitem expressar e verificar propriedades de segurança complexas.

O objetivo é aproximar academia e indústria, demonstrando como assistentes de provas podem ser ferramentas práticas e viáveis para garantir correção em sistemas onde falhas têm consequências financeiras e de segurança significativas, e inspirar novas colaborações entre pesquisa e aplicação industrial.

Implicit Complexity in Reversible Computations

Deivid Vale (Augusta University)

Abstract. Standard programming language semantics are usually uni-directional: computation happens by reducing (evaluating) an expression e to e’, and there is no hope to go backwards. By adding reversibility to a computational model, one can get a fine-grained analysis of its computational behavior. In this talk, I will discuss such behavioral study in the context of complexity analysis. We shall see that by carefully defining a reversible small-step semantics for the lambda-calculus one gets a reversible functional language that are amenable to formalization and reasonable to reason about. Such formalized abstract machine is a novel attempt to bridge the gap between foundational software verification (i.e., formal program analysis on proof assistants) and complexity theory, which up to now has resisted formalization due to technical difficulties on mechanizing complexity-related results constructively. I will show that reversibility is a key component in achieving this herculean task, discuss techniques used to overcome major limitations for a constructive formalization, and the main results I was able to obtain. Mainly: forward reasoning is strategy dependent while backwards computational aren’t. This gives us a forward-nondeterministic language but with backwards determinism. We also show that such language are capable of capturing feasible reversible functions of higher-order polytime.

Title. TBA

Prof. Mauricio Ayala-Rincón(UnB)

Abstract. TBA