3 papers
cs.LO2024
Resource approximation for the -calculus
Davide Barbarossa
The -calculus plays a central role in the theory of programming languages as it extends the Curry-Howard correspondence to classical logic. A major drawback is that it does not…
cs.LO2024
Stability Property for the Call-by-Value -calculus through Taylor Expansion
Davide Barbarossa
We prove the Stability Property for the call-by-value -calculus (CbV in the following). This result states necessary conditions under which the contexts of the CbV -calculus…
cs.LO2024
Denotational semantics driven simplicial homology?
Davide Barbarossa
We look at the proofs of a fragment of Linear Logic as a whole: in fact, Linear Logic's coherent semantics interprets the proofs of a given formula as faces of an abstract simp…