
Resource Transition Systems and Full Abstraction for Linear HigherOrder Effectful Systems
We investigate program equivalence for linear higherorder(sequential) l...
read it

The Space of Interaction (long version)
The space complexity of functional programs is not well understood. In p...
read it

On Measure Quantifiers in FirstOrder Arithmetic (Long Version)
We study the logic obtained by endowing the language of firstorder arit...
read it

On Counting Propositional Logic
We study counting propositional logic as an extension of propositional l...
read it

Modal Reasoning = Metric Reasoning, via Lawvere
Graded modal types systems and coeffects are becoming a standard formali...
read it

The (In)Efficiency of Interaction
Evaluating higherorder functional programs through abstract machines in...
read it

Intersection Types and (Positive) AlmostSure Termination
Randomized higherorder computation can be seen as being captured by a l...
read it

On the Versatility of Open Logical Relations: Continuity, Automatic Differentiation, and a Containment Theorem
Logical relations are one of the most powerful techniques in the theory ...
read it

Decomposing Probabilistic Lambdacalculi
A notion of probabilistic lambdacalculus usually comes with a prescribe...
read it

On HigherOrder Cryptography (Long Version)
Typetwo constructions abound in cryptography: adversaries for encryptio...
read it

The Abstract Machinery of Interaction (Long Version)
This paper revisits the Interaction Abstract Machine (IAM), a machine ba...
read it

A Diagrammatic Calculus for Algebraic Effects
We introduce a new, diagrammatic notation for representing the result of...
read it

Differential Logical Relations, Part I: The SimplyTyped Case (Long Version)
We introduce a new form of logical relation which, in the spirit of metr...
read it

On the Taylor Expansion of Probabilistic λTerms (Long Version)
We generalise Ehrhard and Regnier's Taylor expansion from pure to probab...
read it

The Geometry of Bayesian Programming
We give a geometry of interaction model for a typed lambdacalculus endo...
read it

On the Termination Problem for Probabilistic HigherOrder Recursive Programs
In the last two decades, there has been much progress on model checking ...
read it

On Randomised Strategies in the λCalculus (Long Version)
In this work we introduce randomised reduction strategies, a notion alre...
read it

On Probabilistic Term Rewriting
We study the termination problem for probabilistic term rewrite systems....
read it

Encoding Turing Machines into the Deterministic LambdaCalculus
This note is about encoding Turing machines into the lambdacalculus....
read it
Ugo Dal Lago
is this you? claim profile