31 citations · 68 across the 12 of their papers we have counts for
15 papers · 1 filter
A Reversible Crumbling Abstract Machine for Plotkin's Call-by-Value
Nicolò Pizzo, Claudio Sacerdoti Coen
Landauer's embeddings enable the reversibility of computations for non-reversible programming languages, augmenting each intermediate state with enough data to reconstruct the prev…
Positive Sharing and Abstract Machines
Beniamino Accattoli, Claudio Sacerdoti Coen, Jui-Hsuan Wu
Wu's positive -calculus is a recent call-by-value -calculus with sharing coming from Miller and Wu's study of the proof-theoretical concept of focalization. Accattoli and Wu…
The Cost of Skeletal Call-by-Need, Smoothly
Beniamino Accattoli, Francesco Magliocca, Loïc Peyrot +1
Skeletal call-by-need is an optimization of call-by-need evaluation also known as "fully lazy sharing": when the duplication of a value has to take place, it is first split into "s…
Proceedings Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
Florian Rabe, Claudio Sacerdoti Coen
Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and comput…
IMELL Cut Elimination with Linear Overhead
Beniamino Accattoli, Claudio Sacerdoti Coen
Recently, Accattoli introduced the Exponential Substitution Calculus (ESC) given by untyped proof terms for Intuitionistic Multiplicative Exponential Linear Logic (IMELL), endowed…
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…