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. GencoUltimo
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.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.