HackerPapers

arXiv:1809.03094cs.LO

Classical Proofs as Parallel Programs

Federico Aschieri, Agata Ciabattoni, Francesco Antonio Genco

Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.

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.

arXiv comments
In Proceedings GandALF 2018, arXiv:1809.02416. arXiv admin note: text overlap with arXiv:1607.05120
Journal reference
EPTCS 277, 2018, pp. 43-57
DOI
doi:10.4204/EPTCS.277.4
Subjects
cs.LOLogic in Computer Science

On Hacker News

Linked by 1 identifiable commenter in 1 comment across 1 thread, from May 2020 to May 2020.

Comments linking this paper, per year.

Discussed in comments1 thread

  1. Against Set Theory (2005) [pdf] 1 comment

    • There are a number of different type theory models for classical logic. The first to my knowledge was a model that uses the call-with-current-continuation (call/cc) control flow operator. While this does model classical logic, some say it is not particularly useful as a…

      outlaceView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.