CINECA IRIS Institutional Research Information System
IRIS è il sistema di gestione integrata dei dati della ricerca (persone, progetti, pubblicazioni, attività) adottato dall'Università degli Studi di Torino.
AperTO è l'archivio istituzionale Open Access destinato a raccogliere, rendere visibile e conservare la produzione scientifica dell'Università degli Studi di Torino.
EnglishThe fundamental connection between logic and computation, known as the Curry–Howard correspondence or formulae-as-types and proofs-as-programs paradigm, relates logical and computational systems. We present an overview of computational interpretations of intuitionistic and classical logic: • intuitionistic natural deduction - λ-calculus • intuitionistic sequent calculus - λGtz-calculus • classical natural deduction - λµ-calculus • classical sequent calculus - λµµ~-calculus. In this work we summarise the authors’ contributions in this field. Fundamental properties of these calculi, such as confluence, normalisation properties, reduction strategies call-by-value and call-by-name, separability, reducibility method, λ-models are in focus. These fundamental properties and their counterparts in logics, via the Curry– Howard correspondence, are discussed.
Computational Interpretations of Logics / Silvia Ghilezan; Silvia Likavec. - In: ZBORNIK RADOVA. - ISSN 0351-9406. - 12(20)(2009), pp. 159-215.
| Titolo: | Computational Interpretations of Logics | |
| Autori Riconosciuti: | ||
| Autori: | Silvia Ghilezan; Silvia Likavec | |
| Data di pubblicazione: | 2009 | |
| Abstract: | The fundamental connection between logic and computation, known as the Curry–Howard correspondence or formulae-as-types and proofs-as-programs paradigm, relates logical and computational systems. We present an overview of computational interpretations of intuitionistic and classical logic: • intuitionistic natural deduction - λ-calculus • intuitionistic sequent calculus - λGtz-calculus • classical natural deduction - λµ-calculus • classical sequent calculus - λµµ~-calculus. In this work we summarise the authors’ contributions in this field. Fundamental properties of these calculi, such as confluence, normalisation properties, reduction strategies call-by-value and call-by-name, separability, reducibility method, λ-models are in focus. These fundamental properties and their counterparts in logics, via the Curry– Howard correspondence, are discussed. | |
| Volume: | 12(20) | |
| Pagina iniziale: | 159 | |
| Pagina finale: | 215 | |
| URL: | http://elib.mi.sanu.ac.rs/files/journals/zr/20/n020p159.pdf | |
| Rivista: | ZBORNIK RADOVA | |
| Appare nelle tipologie: | 03A-Articolo su Rivista |
File in questo prodotto:
| File | Descrizione | Tipologia | Licenza | |
|---|---|---|---|---|
| Silviae_4aperto.pdf | POSTPRINT (VERSIONE FINALE DELL’AUTORE) | Open Access Visualizza/Apri |
Copyright © 2021