4 papers
When Types Intersect and Effects Get Handled
Stefano Catozi, Ugo Dal Lago, Taro Sekiyama
We introduce a novel intersection type system for a -calculus with algebraic effects and handlers. The system, inherently behavioral in nature, enjoys the classical properties o…
Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages
Andrea Colledan, Ugo Dal Lago
We introduce a type system for the Quipper language designed to derive upper bounds on the size of the circuits produced by the typed program. This size can be measured according t…
On Computational Indistinguishability and Logical Relations
Ugo Dal Lago, Zeinab Galal, Giulia Giusti
A -calculus is introduced in which all programs can be evaluated in probabilistic polynomial time and in which there is sufficient structure to represent sequential cryptographi…
On Separation Logic, Computational Independence, and Pseudorandomness (Extended Version)
Ugo Dal Lago, Davide Davoli, Bruce M. Kapron
Separation logic is a substructural logic which has proved to have numerous and fruitful applications to the verification of programs working on dynamic data structures. Recently,…