2018/09/07 by Federico Aschieri, Agata Ciabattoni, Francesco A. Genco +1
Computer Science · Mathematics · #Broadcasting (networking) #Calculus (dental) #Computer science #First-order logic #Formal Methods in Verification #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Mathematical proof #Mathematics #Natural deduction #Normalization (sociology) #Programming language #Theoretical computer science #cs.LO
paper · pdf · doi:10.4204/eptcs.277.4
published as EPTCS 277, 2018, pp. 43-57 · In Proceedings GandALF 2018, arXiv:1809.02416. arXiv admin note: text overlap with arXiv:1607.05120
openalex publication_date 2018/09/07 · arxiv created 2018/09/10 · arxiv updated 2018/09/24 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/06
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.