Seminario
Logic and Algebra in Computer Science: a dual perspective
Abstract dell'evento
This presentation serves a dual purpose. Firstly, we delve into the computational interpretations of intuitionistic logic (Curry-Howard correspondence) and classical logic (Griffin-Krivine correspondence). Secondly, we explore the application of algebraic methods in computer science.
The Curry-Howard (or proof-as-program) correspondence expresses the conceptual alignment between proof theory and programming language theory. It appears at many levels, for instance at the specification level where formulæ are types, and at the term level where proofs are programs. In this perspective, executing a program becomes a logical transformation known as cut elimination. However, a significant limitation to this correspondence exists: it is confined to constructive logic, where proofs explicitly construct the objects they introduce.
A pivotal breakthrough occurred in nineties when Timothy Griffin removed this restriction, extending the correspondence to classical logic through the introduction of the call-cc control operator, which captures the state of the environment. Intuitively, call-cc allows us to rewind to a previous point in the program, making an alternate choice or taking a different execution path. Griffin was the first to type a control operator, a notable achievement as it connects call-cc and Peirce’s law of classical logic, both known for decades, revealing a profound connection that had gone unnoticed. Subsequent to this discovery, various techniques have been employed to incorporate classical logic into computation.
In the last part of this presentation, we present a research program initiated by the author in the late nineties. This program aims to explore lambda calculus and combinatory logic through the application of universal algebra techniques.
Relatori/Relatrici
Antonino Salibra, Full Professor of Computer Science at Ca' Foscari University of Venice (Italy).
Dettagli sull'evento
Data e luogo
Inizio: 12/02/2024
alle ore 16:00
Fine: 12/02/2024
alle ore 18:00
Palazzo Albani (Urbino, Via Viti, 10) Aula D1
Organizzato e promosso da:
Dipartimento di Scienze Pure e Applicate
Modalità di partecipazione
Altre informazioni utili
Ingresso libero
