Classical proofs as parallel programs

MaRDI QIDQ3384877zbMATH OpenFDO

Authors Federico Aschieri, Agata Ciabattoni, Francesco A. Genco

Publication date 17 December 2021

Full work available at URL https://arxiv.org/abs/1809.03094, http://eptcs.web.cse.unsw.edu.au/paper.cgi?GandALF18.4

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Applications of game theory (91A80)

Recommendations

• scientific article; zbMATH DE number 517083
• Programming and Proving with Classical Types
• scientific article; zbMATH DE number 1104448
• Non deterministic classical logic: the $\lambda\mu^{++}$-calculus

Cites work

• Call-by-value is dual to call-by-name
• Functions as processes
• Gödel logic. From natural deduction to parallel computation
• Higher-order processes, functions, and sessions: a monadic integration
• scientific article; zbMATH DE number 1670484 (Why is no real title available?)
• scientific article; zbMATH DE number 2185662 (Why is no real title available?)
• scientific article; zbMATH DE number 5851813 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 46869 (Why is no real title available?)
• scientific article; zbMATH DE number 1390069 (Why is no real title available?)
• scientific article; zbMATH DE number 3358455 (Why is no real title available?)
• Lectures on the Curry-Howard isomorphism
• Proofs of strong normalisation for second order classical natural deduction
• Propositions as sessions
• The duality of computation
• The lambda calculus. Its syntax and semantics. Rev. ed.

Cited in

(6)

• On the concurrent computational content of intermediate logics
• Normality, non-contamination and logical depth in classical natural deduction
• Proof spaces for unbounded parallelism
• scientific article; zbMATH DE number 2213623 (Why is no real title available?)
• What stands between grounding rules and logical rules is the excluded middle
• A typed parallel -calculus via 1-depth intermediate proofs

This page was built for publication: Classical proofs as parallel programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3384877)