07/02/2025, 16:00 — 17:00 — Sala P3.10, Pavilhão de Matemática Online
José Espírito Santo, Departamento de Matemática e Centro de Matemática, Universidade do Minho
An extension of the Curry-Howard correspondence to proof search
A proof is the successful outcome of a proof search run, and such outcome is conveniently represented by a lambda-term. More generally, runs of goal-directed proof search are possibly infinite and are conveniently represented by terms of the coinductive lambda-calculus. For some logics, there is an equivalent, finitary representation, making use of formal fixed points. On such syntax one can base a new approach to the study of proof search. We will review the case study of intuitionistic implicational logic, that is, the theory of simple types. We will consider decision problems (existence of inhabitants, several concepts of finiteness), coherence questions about the uniqueness of inhabitants, and situations where a type either is empty of has infinitely many inhabitants. This is joint work with Ralph Matthes and Luís Pinto.
