43 citations · 77 across the 16 of their papers we have counts for
17 papers
$\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 III: The Strange Case of the Intuitionistic Logic of Constant Domains
Federico Aschieri
The logic of constant domains is intuitionistic logic extended with the so-called forall-shift axiom, a classically valid statement which implies the excluded middle over decidable…
Expansion Trees with Cut
Federico Aschieri, Stefan Hetzl, Daniel Weller
Herbrand's theorem is one of the most fundamental insights in logic. From the syntactic point of view, it suggests a compact representation of proofs in classical first- and higher…