On the Concurrent Computational Content of Intermediate Logics
Theoretical Computer Science, pp. 375-409, 2020.
Abstract We provide a proofs-as-concurrent-programs interpretation for a large class of intermediate logics that can be formalized by cut-free hypersequent calculi. Obtained by adding classical disjunctive tautologies to intuitionistic logic, these logics are used to type concurrent λ-calculi by Curry–Howard correspondence; each of the ...More
Full Text (Upload PDF)
PPT (Upload PPT)