9 citations · 23 across the 13 of their papers we have counts for
13 papers
A Direct Characterisation of Logical Grounds and a Decidability Proof
Francesco A. Genco
We present a standard calculus for logical grounding based on well-established grounding principles [Schnieder, 2011, Fine, 2012, Correia, 2014, Correia, 2024] and provide a very d…
Evaluating AI fairness in credit scoring with the BRIO tool
Greta Coraglia, Francesco A. Genco, Pellegrino Piantadosi +4
We present a method for quantitative, in-depth analyses of fairness issues in AI systems with an application to credit scoring. To this aim we use BRIO, a tool for the evaluation o…
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…
Grounding Operators: Transitivity and Trees, Logicality and Balance
Francesco A. Genco
We formally investigate immediate and mediate grounding operators from an inferential perspective. We discuss the differences in behaviour displayed by several grounding operators…
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…
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…
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…