The Colloquium of Logic is organized by the Portuguese Logic Society and aims to promote the research and knowledge in this field, from mathematical logic to philosophical logic as well as logic for artificial intelligence and theoretical computer science. The talks of the Colloquium of Logic will be held in a hybrid way. The talks will take place at the Mathematics Department of Técnico ULisboa, room 3.10, and virtually on Zoom. The next speaker is:
- José Espírito Santo (Department of Mathematics and Centre of Mathematics, UMinho), “An extension of the Curry-Howard correspondence to proof search”, 7th February 2025, 16:00
Abstract: 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.