Ugo Dal Lago

The Abstract Machinery of Interaction (Long Version).

2020 · arXiv (Cornell University)

This paper revisits the Interaction Abstract Machine (IAM), a machine based on Girard's Geometry of Interaction, introduced by Mackie and Danos & Regnier. It is an unusual machine, not relying on environments, presented on linear …

Circuit Width Estimation via Effect Typing and Linear Dependency (Long Version)

2023 · arXiv (Cornell University)

Circuit description languages are a class of quantum programming languages in which programs are classical and produce a description of a quantum computation, in the form of a quantum circuit. Since these programs can leverage …

On the Almost-Sure Termination of Binary Sessions

2024

We investigate the termination problem in a calculus of sessions with probabilistic choices. In this setting, a whole range of termination properties can be defined, from the weaker almost-sure termination to strong almost-sure termination, passing …

On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs

2025 · Proceedings of the ACM on Programming Languages

Applying higher-order model checking techniques to programs that use effect handlers is a major challenge, given the recent undecidability result obtained by Dal Lago and Ghyselen. This challenge has been addressed by using answer-type modifications, …