9 citations · 23 across the 13 of their papers we have counts for
8 papers · 1 filter
A Strongly Normalising System of Dependent Types for Transparent and Opaque Probabilistic Computation
Francesco A. Genco
We define an extension of lambda-calculus with dependents types that enables us to encode transparent and opaque probabilistic programs and prove a strong normalisation result for…
A Logic of Knowledge and Justifications, with an Application to Computational Trust
Francesco A. Genco
We present a logical framework that enables us to define a formal theory of computational trust in which this notion is analysed in terms of epistemic attitudes towards the possibl…
A Typed Lambda-Calculus for Establishing Trust in Probabilistic Programs
Francesco A. Genco, Giuseppe Primiero
The extensive deployment of probabilistic algorithms has radically changed our perspective on several well-established computational notions. Correctness is probably the most basic…
$\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…
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…
Gödel Logic: from Natural Deduction to Parallel Computation
Federico Aschieri, Agata Ciabattoni, Francesco A. Genco
Propositional Gödel logic extends intuitionistic logic with the non-constructive principle of linearity . We introduce a Curry-Howard correspo…