Università degli Studi di Urbino Carlo Bo / Portale Web di Ateneo


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

partecipa su zoom

Altre informazioni utili

Ingresso libero


Link e risorse utili

clicca qui  aggiungi al calendario

Il tuo 5x1000 per sostenere le attività di ricerca

L'Università di Urbino destina tutte le risorse che deriveranno da questa iniziativa alla ricerca scientifica ed al sostegno di giovani ricercatori.

15 22

Se sei vittima di violenza o stalking chiama il 1522, scarica l'app o chatta su www.1522.eu

Il numero, gratuito è attivo 24 h su 24, accoglie con operatrici specializzate le richieste di aiuto e sostegno delle vittime di violenza e stalking.

Posta elettronica certificata

amministrazione@uniurb.legalmail.it

Social

Università degli Studi di Urbino Carlo Bo
Via Aurelio Saffi, 2 – 61029 Urbino PU – IT
Partita IVA 00448830414 – Codice Fiscale 82002850418
2024 © Tutti i diritti sono riservati

Top