Eventos

Linear logic (LL) has been used as a foundation (and inspiration) for the development of programming languages, logical frameworks and models for concurrency. In this talk, we shall see how to use the meta-theory of LL to (semi-automatically) prove the cut-elimination theorem for different object logics (OL) including propositional classical, minimal and intuitionistic logics. By considering a variant of LL with subexponentials, it is possible to extend these results to a wider range of logics including the modal logics K, 4, KT, KD and S4.

Os problemas equacionais são cruciais em matemática, computação e suas aplicações. Esses problemas são geralmente formulados sobre linguagens com operadores que satisfazem propriedades algébricas simples, tais como associatividade (p.ex., concatenação de palavras, relações de parentesco, multiplicação matricial, etc.) e comutatividade (p.ex., operações aritméticas de soma e multiplicação, etc.). Tais propriedades devem ser implementadas na base de sistemas algébricos, simbólicos, dedutivos e, em geral computacionais, de forma correta e eficiente. A palestra irá rever problemas como ‘verificação da igualdade’, ‘casamento’ e ‘unificação’ módulo teorias equacionais e discutir o desenvolvimento em curso de uma abordagem sintático-lógica, denominada “nominal”, desses problemas.

The notion of linearisation of the lambda-calculus has been explored in different settings: Damas and Florido used information given by intersection types, to define a notion of expansion of terms in the lambda-calculus into linear terms; Kfoury embedded the lambda-calculus into a new linear calculus, with a new notion of “linear” reduction, and linearization was defined indirectly by means of a notion of contraction of expanded terms in the new calculus into standard lambda-terms; Alves and Florido defined a notion of linearisation from standard lambda-terms into a linear subset, called the weak linear lambda-calculus, by using the notion of computation as paths, deriving from Lévy’s labelled lambda-calculus.

$\lambda$-terms can be syntactically represented in different ways than the usual term strings; for example, one can use combinators, string diagrams and for the linear case Zeilberger’s trivalent maps. The main purpose of this paper is to study the relation between arbitrary $\lambda$-terms and maps over orientable surfaces contained in $\mathbb{R}^3$. For this reason, topological graphs are introduced. These graphs include free-edges and hyper-edges to represent, respectively, free and multiple occurrences of variables.

Process calculi are expressive specification languages for concurrency. They have been very successful in two research strands: the analysis of security protocols and the enforcement of correct message-passing programs. Despite their shared foundations, languages and reasoning techniques for (1) and (2) have been separately developed. Here we connect two representative calculi from (1) and (2): we encode a (high-level) pi-calculus for multiparty sessions into a (low-level) applied pi-calculus for security protocols.

O PVS (Prototype Verification System) é um sistema de especificação e verificação formal, desenvolvido por SRI International, que provê um ambiente integrado para desenvolvimento e análise de especificações formais, com suporte a uma ampla gama de atividades envolvendo criação, análise, modificação, gerenciamento e documentação de teorias e provas. O PVS é uma ferramenta fundamental em vários projetos envolvendo verificação formal desenvolvidos pelo grupo de métodos formais do NASA Langley Research Center (NASA LaRC), por essa razão existe um esforço contínuo dos pesquisadores do NASA LaRC no sentido de desenvolver técnicas de verificação formal integradas ao PVS visando uma variedade de aplicações, originando assim uma grande coleção de teorias envolvendo verificações formais importantes que vão desde teorias matemáticas complexas em álgebra, análise e teoria de conjuntos por exemplo, até especificações e formalizações de modelos para a verificação de sistemas de tráfego aéreo e de protocolos de tolerância a falhas.

Although it is well-known that termination is an undecidable property of programs, there are several efforts related with automating the termination of specifications with two main objectives: to develop compilers that might provide warnings of possible non-termination and to increase the grade of automation of proof assistants and deductive systems. In this talk, a general view will be given of the (Prototype Verification System) PVS theories for automating termination developed by members of the Group of Theory of Computation at the Universidade de Brasília and collaborators.

Is computation a new or an old phenomenon? The word algorithm (although named after Alkhawarizmi), is not hundreds of years old. It is thousands of years old. Although computers were only invented in the 20th century, computation is a very old phenomenon. In this talk, we discuss the evolution of the concept of computation from a logical point of view.