43 citations · 77 across the 16 of their papers we have counts for
12 papers · 1 filter
$\unicode{8523}$ means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs
Federico Aschieri, Francesco A. Genco
Along the lines of the Abramsky ``Proofs-as-Processes'' program, we present an interpretation of multiplicative linear logic as typing system for concurrent functional programming.…
Natural Deduction and Normalization Proofs for the Intersection Type Discipline
Federico Aschieri
Refining and extending previous work by Retoré, we develop a systematic approach to intersection types via natural deduction. We show how a step of beta reduction can be seen as pe…
A typed parallel λ-calculus via 1-depth intermediate proofs
Federico Aschieri, Agata Ciabattoni, Francesco A. Genco
We introduce a Curry-Howard correspondence for a large class of intermediate logics characterized by intuitionistic proofs with non-nested applications of rules for classical disju…
Classical Proofs as Parallel Programs
Federico Aschieri, Agata Ciabattoni, Francesco Antonio Genco
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 correspond…
On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic
Federico Aschieri, Matteo Manighetti
Intuitionistic first-order logic extended with a restricted form of Markov's principle is constructive and admits a Curry-Howard correspondence, as shown by Herbelin. We provide a…
On Natural Deduction for Herbrand Constructive Logics I: Curry-Howard Correspondence for Dummett's Logic LC
Federico Aschieri
Dummett's logic LC is intuitionistic logic extended with Dummett's axiom: for every two statements the first implies the second or the second implies the first. We present a natura…