Classical Proofs as Parallel Programs
| Autor: | Aschieri, Federico, Ciabattoni, Agata, Genco, Francesco Antonio |
|---|---|
| Rok vydání: | 2018 |
| Předmět: | |
| Zdroj: | EPTCS 277, 2018, pp. 43-57 |
| Druh dokumentu: | Working Paper |
| DOI: | 10.4204/EPTCS.277.4 |
| Popis: | We introduce a first proofs-as-parallel-programs correspondence for classical logic. We define a parallel and more powerful extension of the simply typed lambda calculus corresponding to an analytic natural deduction based on the excluded middle law. The resulting functional language features a natural higher-order communication mechanism between processes, which also supports broadcasting. The normalization procedure makes use of reductions that implement novel techniques for handling and transmitting process closures. Comment: In Proceedings GandALF 2018, arXiv:1809.02416. arXiv admin note: text overlap with arXiv:1607.05120 |
| Databáze: | arXiv |
| Externí odkaz: |
|