4 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…