9 citations · 9 across the 2 of their papers we have counts for
6 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.…
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…
Hypersequents and Systems of Rules: Embeddings and Applications
Agata Ciabattoni, Francesco A. Genco
We define a bi-directional embedding between hypersequent calculi and a subclass of systems of rules (2-systems). In addition to showing that the two proof frameworks have the same…
Disjunctive Axioms and Concurrent -Calculi: a Curry-Howard Approach
F. Aschieri, A. Ciabattoni, F. A. Genco
We add to intuitionistic logic infinitely many classical disjunctive tautologies and use the Curry--Howard correspondence to obtain typed concurrent -calculi; each of them featu…
Mīmā\d{m}sā deontic logic: proof theory and applications
Agata Ciabattoni, Elisa Freschi, Francesco A. Genco +1
Starting with the deontic principles in M\=ımā\d{m}sā texts we introduce a new deontic logic. We use general proof-theoretic methods to obtain a cut-free sequent calculus for this…