2 citations · 2 across the 2 of their papers we have counts for
5 papers
Strong Call-by-Value is Reasonable, Implosively
Beniamino Accattoli, Andrea Condoluci, Claudio Sacerdoti Coen
Whether the number of beta-steps in the lambda-calculus can be taken as a reasonable time cost model (that is, polynomially related to the one of Turing machines) is a delicate pro…
Sharing Equality is Linear
Andrea Condoluci, Beniamino Accattoli, Claudio Sacerdoti Coen
The -calculus is a handy formalism to specify the evaluation of higher-order programs. It is not very handy, however, when one interprets the specification as an execution mecha…
Crumbling Abstract Machines
Beniamino Accattoli, Andrea Condoluci, Giulio Guerrieri +1
Extending the lambda-calculus with a construct for sharing, such as let expressions, enables a special representation of terms: iterated applications are decomposed by introducing…
Admissible Tools in the Kitchen of Intuitionistic Logic
Andrea Condoluci, Matteo Manighetti
The usual reading of logical implication "A implies B" as "if A then B" fails in intuitionistic logic: there are formulas A and B such that "A implies B" is not provable, even thou…
CERES in Propositional Proof Schemata
Andrea Condoluci
Cut-elimination is one of the most famous problems in proof theory, and it was defined and solved for first-order sequent calculus by Gentzen in his celebrated Hauptsatz. Ceres is…