research
∙
08/31/2023
On Model-Checking Higher-Order Effectful Programs (Long Version)
Model-checking is one of the most powerful techniques for verifying syst...
share
research
∙
07/14/2023
Contextual Behavioural Metrics (Extended Version)
We introduce contextual behavioural metrics (CBMs) as a novel way of mea...
research
∙
02/10/2023
On the Lattice of Program Metrics
In this paper we are concerned with understanding the nature of program ...
research
∙
01/29/2023
A Log-Sensitive Encoding of Turing Machines in the λ-Calculus
This note modifies the reference encoding of Turing machines in the λ-ca...
research
∙
01/27/2023
An Arithmetic Theory for the Poly-Time Random Functions
We introduce a new bounded theory RS^1_2 and show that the functions whi...
research
∙
11/12/2022
Open Higher-Order Logic (Long Version)
We introduce a variation on Barthe et al.'s higher-order logic in which ...
research
∙
07/21/2022
On Feller Continuity and Full Abstraction (Long Version)
We study the nature of applicative bisimilarity in λ-calculi endowed wit...
research
∙
07/18/2022
Multi Types and Reasonable Space (Long Version)
Accattoli, Dal Lago, and Vanoni have recently proved that the space used...
research
∙
07/07/2022
On Session Typing, Probabilistic Polynomial Time, and Cryptographic Experiments (Long Version)
A system of session types is introduced as induced by a Curry Howard cor...
research
∙
04/28/2022
On Quantitative Algebraic Higher-Order Theories
We explore the possibility of extending Mardare et al. quantitative alge...
research
∙
03/29/2022
On Reinforcement Learning, Effect Handlers, and the State Monad
We study the algebraic effects and handlers as a way to support decision...
research
∙
03/21/2022
Curry and Howard Meet Borel
We show that an intuitionistic version of counting propositional logic c...
research
∙
03/01/2022
Reasonable Space for the λ-Calculus, Logarithmically
Can the λ-calculus be considered as a reasonable computational model? Ca...
research
∙
02/15/2022
On Dynamic Lifting and Effect Typing in Circuit Description Languages (Extended Version)
In the realm of quantum computing, circuit description languages represe...
research
∙
12/28/2021
Proceedings Second Joint International Workshop on Linearity Trends in Linear Logic and Applications
This volume contains a selection of papers presented at Linearity TLLA...
research
∙
06/24/2021
Resource Transition Systems and Full Abstraction for Linear Higher-Order Effectful Systems
We investigate program equivalence for linear higher-order(sequential) l...
research
∙
04/28/2021
The Space of Interaction (long version)
The space complexity of functional programs is not well understood. In p...
research
∙
04/25/2021
On Measure Quantifiers in First-Order Arithmetic (Long Version)
We study the logic obtained by endowing the language of first-order arit...
research
∙
03/23/2021
On Counting Propositional Logic
We study counting propositional logic as an extension of propositional l...
research
∙
03/05/2021
Modal Reasoning = Metric Reasoning, via Lawvere
Graded modal types systems and coeffects are becoming a standard formali...
research
∙
10/24/2020
The (In)Efficiency of Interaction
Evaluating higher-order functional programs through abstract machines in...
research
∙
10/23/2020
Intersection Types and (Positive) Almost-Sure Termination
Randomized higher-order computation can be seen as being captured by a l...
research
∙
02/19/2020
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 ...
research
∙
02/19/2020
Decomposing Probabilistic Lambda-calculi
A notion of probabilistic lambda-calculus usually comes with a prescribe...
research
∙
02/17/2020
On Higher-Order Cryptography (Long Version)
Type-two constructions abound in cryptography: adversaries for encryptio...
research
∙
02/13/2020
The Abstract Machinery of Interaction (Long Version)
This paper revisits the Interaction Abstract Machine (IAM), a machine ba...
research
∙
01/05/2020
A Diagrammatic Calculus for Algebraic Effects
We introduce a new, diagrammatic notation for representing the result of...
research
∙
04/27/2019
Differential Logical Relations, Part I: The Simply-Typed Case (Long Version)
We introduce a new form of logical relation which, in the spirit of metr...
research
∙
04/21/2019
On the Taylor Expansion of Probabilistic λ-Terms (Long Version)
We generalise Ehrhard and Regnier's Taylor expansion from pure to probab...
research
∙
04/16/2019
The Geometry of Bayesian Programming
We give a geometry of interaction model for a typed lambda-calculus endo...
research
∙
11/06/2018
On the Termination Problem for Probabilistic Higher-Order Recursive Programs
In the last two decades, there has been much progress on model checking ...
research
∙
05/10/2018
On Randomised Strategies in the λ-Calculus (Long Version)
In this work we introduce randomised reduction strategies, a notion alre...
research
∙
02/27/2018
On Probabilistic Term Rewriting
We study the termination problem for probabilistic term rewrite systems....
research
∙
11/28/2017