Title: Intermediate logics and concurrent λ-calculi: a proof-theoretical approach
Language: English
Authors: Genco, Francesco Antonio 
Qualification level: Doctoral
Keywords: Proof theory; Intermediate logics; proofs-as-programs; natural deduction; lambda-calculus; parallelism; concurrency
Advisor: Ciabattoni, Agata 
Issue Date: 2019
Number of Pages: 197
Qualification level: Doctoral
Avron speculated in 1991 that the proof-theoretical formalism of hypersequents might be connected with concurrent computation and that it should be possible to use the intermediate logics that can be naturally captured by hypersequent calculi as bases for parallel -calculi. We define parallel and concurrent -calculi based on CurryHoward correspondences for intermediate logics that can be formalized as hypersequent calculi. The introduced calculi are more expressive than simply-typed -calculus and can formalize interesting parallel and concurrent programs. We thus confirm Avrons thesis. In order to do so, we first provide a general translation from hypersequent calculi to suitable natural deduction calculi. We then use the obtained proof systems for classical and GodelDummett logic to define the first concurrent computational interpretations of these well-known logics. The resulting calculi Cl and G are concurrent extensions of simply typed -calculus. We then introduce , a parallel extension of simply typed -calculus. Its type system is based on an infinite set of axioms corresponding to hypersequent rules and can be used to type terms that correspond to generic communication topologies. We prove strong normalization for and showcase its expressive power by programming examples. Since the type system of only corresponds to a fragment of the considered intermediate logics, we also provide a concurrent computational interpretation for the full logical systems. The normalization of the resulting calculi require general communication reductions also featured in Cl and G that ensure that the subformula property holds and implement code mobility techniques for function closure transmission.
URI: https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-124913
Library ID: AC15366548
Organisation: E192 - Institut für Logic and Computation 
Publication Type: Thesis
Appears in Collections:Thesis

Files in this item:

Show full item record

Page view(s)

checked on Feb 18, 2021


checked on Feb 18, 2021

Google ScholarTM


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.