Propositional Gödel logic G extends intuitionistic logic with the non-constructive principle of linearity (A → B) ∨ (B → A). We introduce a Curry-Howard correspondence for G and show that a simple natural deduction calculus can be used as a typing system. The resulting functional language extends the simply typed λ-calculus via a synchronous communication mechanism between parallel processes, which increases its expressive power. The normalization proof employs original termination arguments and proof transformations implementing forms of code mobility. Our results provide a computational interpretation of G, thus proving A. Avron's 1991 thesis.

Gödel logic: From natural deduction to parallel computation / F. Aschieri, A. Ciabattoni, F.A. Genco (PROCEEDINGS - SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE). - In: LICS[s.l] : Institute of Electrical and Electronics Engineers (IEEE), 2017. - ISBN 9781509030187. - pp. 1-12 (( Intervento presentato al 32. convegno Annual ACM/IEEE Symposium on Logic in Computer Science : 20 through 23 June tenutosi a Reykjavik nel 2017 [10.1109/lics.2017.8005076].

Gödel logic: From natural deduction to parallel computation

F.A. Genco
Ultimo
2017

Abstract

Propositional Gödel logic G extends intuitionistic logic with the non-constructive principle of linearity (A → B) ∨ (B → A). We introduce a Curry-Howard correspondence for G and show that a simple natural deduction calculus can be used as a typing system. The resulting functional language extends the simply typed λ-calculus via a synchronous communication mechanism between parallel processes, which increases its expressive power. The normalization proof employs original termination arguments and proof transformations implementing forms of code mobility. Our results provide a computational interpretation of G, thus proving A. Avron's 1991 thesis.
Settore M-FIL/02 - Logica e Filosofia della Scienza
2017
Institute of Electrical and Electronics Engineers (IEEE)
Association for Computing Machinery (ACM)
Book Part (author)
File in questo prodotto:
File Dimensione Formato  
LICS 2017.pdf

accesso riservato

Tipologia: Publisher's version/PDF
Dimensione 855.95 kB
Formato Adobe PDF
855.95 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
1607.05120.pdf

accesso aperto

Tipologia: Pre-print (manoscritto inviato all'editore)
Dimensione 690.28 kB
Formato Adobe PDF
690.28 kB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/1035230
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 11
  • ???jsp.display-item.citation.isi??? 1
social impact