Classical Proofs as Parallel Programs
Logic in Computer Science
2018-09-24 v1
Abstract
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.
Cite
@article{arxiv.1809.03094,
title = {Classical Proofs as Parallel Programs},
author = {Federico Aschieri and Agata Ciabattoni and Francesco Antonio Genco},
journal= {arXiv preprint arXiv:1809.03094},
year = {2018}
}
Comments
In Proceedings GandALF 2018, arXiv:1809.02416. arXiv admin note: text overlap with arXiv:1607.05120