Theory of Computation

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.

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.

Title: TBA

Prof. Jorge A. Pérez (UGroningen)

Abstract. TBA

Title. TBA

Prof. Rodrigo Ribeiro (UFOP)

Abstract. TBA

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