Ugo Dal Lago

Orcid: 0000-0001-9200-070X

Affiliations:
  • Università degli Studi di Bologna, Italy


According to our database1, Ugo Dal Lago authored at least 172 papers between 2001 and 2024.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
On Model-Checking Higher-Order Effectful Programs.
Proc. ACM Program. Lang., January, 2024

On Basic Feasible Functionals and the Interpretation Method.
Proceedings of the Foundations of Software Science and Computation Structures, 2024

Circuit Width Estimation via Effect Typing and Linear Dependency.
Proceedings of the Programming Languages and Systems, 2024

Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories.
Proceedings of the 32nd EACSL Annual Conference on Computer Science Logic, 2024

2023
On counting propositional logic and Wagner's hierarchy.
Theor. Comput. Sci., 2023

Preface to the special issue on metric and differential semantics.
Math. Struct. Comput. Sci., 2023

Circuit Width Estimation via Effect Typing and Linear Dependency (Long Version).
CoRR, 2023

On Model-Checking Higher-Order Effectful Programs (Long Version).
CoRR, 2023

Contextual Behavioural Metrics (Extended Version).
CoRR, 2023

A Log-Sensitive Encoding of Turing Machines in the λ-Calculus.
CoRR, 2023

An Arithmetic Theory for the Poly-Time Random Functions.
CoRR, 2023

(Not So) Boring Abstract Machines.
Proceedings of the 24th Italian Conference on Theoretical Computer Science, 2023

On the Lattice of Program Metrics.
Proceedings of the 8th International Conference on Formal Structures for Computation and Deduction, 2023

Open Higher-Order Logic.
Proceedings of the 31st EACSL Annual Conference on Computer Science Logic, 2023

Contextual Behavioural Metrics.
Proceedings of the 34th International Conference on Concurrency Theory, 2023

2022
Implicit computation complexity in higher-order programming languages: A Survey in Memory of Martin Hofmann.
Math. Struct. Comput. Sci., June, 2022

A relational theory of effects and coeffects.
Proc. ACM Program. Lang., 2022

Effectful program distancing.
Proc. ACM Program. Lang., 2022

On Feller continuity and full abstraction.
Proc. ACM Program. Lang., 2022

Multi types and reasonable space.
Proc. ACM Program. Lang., 2022

Open Higher-Order Logic (Long Version).
CoRR, 2022

On Feller Continuity and Full Abstraction (Long Version).
CoRR, 2022

Multi Types and Reasonable Space (Long Version).
CoRR, 2022

On Session Typing, Probabilistic Polynomial Time, and Cryptographic Experiments (Long Version).
CoRR, 2022

On Reinforcement Learning, Effect Handlers, and the State Monad.
CoRR, 2022

On Dynamic Lifting and Effect Typing in Circuit Description Languages (Extended Version).
CoRR, 2022

Implicit recursion-theoretic characterizations of counting classes.
Arch. Math. Log., 2022

On Dynamic Lifting and Effect Typing in Circuit Description Languages.
Proceedings of the 28th International Conference on Types for Proofs and Programs, 2022

Curry and Howard Meet Borel.
Proceedings of the LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2, 2022

Reasonable Space for the λ-Calculus, Logarithmically.
Proceedings of the LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2, 2022

On Quantitative Algebraic Higher-Order Theories.
Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction, 2022

On Session Typing, Probabilistic Polynomial Time, and Cryptographic Experiments.
Proceedings of the 33rd International Conference on Concurrency Theory, 2022

Tidy: Symbolic Verification of Timed Cryptographic Protocols.
Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, 2022

2021
Differential logical relations, part II increments and derivatives.
Theor. Comput. Sci., 2021

Intersection types and (positive) almost-sure termination.
Proc. ACM Program. Lang., 2021

On continuation-passing transformations and expected cost analysis.
Proc. ACM Program. Lang., 2021

The (In)Efficiency of interaction.
Proc. ACM Program. Lang., 2021

The geometry of Bayesian programming.
Math. Struct. Comput. Sci., 2021

On Higher-Order Probabilistic Subrecursion.
Log. Methods Comput. Sci., 2021

Resource Transition Systems and Full Abstraction for Linear Higher-Order Effectful Systems.
CoRR, 2021

The Space of Interaction (long version).
CoRR, 2021

On Measure Quantifiers in First-Order Arithmetic (Long Version).
CoRR, 2021

On Counting Propositional Logic.
CoRR, 2021

Modal Reasoning = Metric Reasoning, via Lawvere.
CoRR, 2021

A Recursion-Theoretic Characterization of the Probabilistic Class PP.
Proceedings of the 46th International Symposium on Mathematical Foundations of Computer Science, 2021

The Space of Interaction.
Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, 2021

Resource Transition Systems and Full Abstraction for Linear Higher-Order Effectful Programs.
Proceedings of the 6th International Conference on Formal Structures for Computation and Deduction, 2021

On Measure Quantifiers in First-Order Arithmetic.
Proceedings of the Connecting with Computability, 2021

2020
On randomised strategies in the <i>λ</i>-calculus.
Theor. Comput. Sci., 2020

Effectful applicative similarity for call-by-name lambda calculi.
Theor. Comput. Sci., 2020

On probabilistic term rewriting.
Sci. Comput. Program., 2020

On the Termination Problem for Probabilistic Higher-Order Recursive Programs.
Log. Methods Comput. Sci., 2020

On Higher-Order Cryptography (Long Version).
CoRR, 2020

The Abstract Machinery of Interaction (Long Version).
CoRR, 2020

A Diagrammatic Calculus for Algebraic Effects.
CoRR, 2020

The Machinery of Interaction.
Proceedings of the PPDP '20: 22nd International Symposium on Principles and Practice of Declarative Programming, 2020

On Higher-Order Cryptography.
Proceedings of the 47th International Colloquium on Automata, Languages, and Programming, 2020

Solvability in a Probabilistic Setting (Invited Talk).
Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, 2020

Decomposing Probabilistic Lambda-Calculi.
Proceedings of the Foundations of Software Science and Computation Structures, 2020

On the Versatility of Open Logical Relations - Continuity, Automatic Differentiation, and a Containment Theorem.
Proceedings of the Programming Languages and Systems, 2020

2019
Probabilistic Termination by Monadic Affine Sized Typing.
ACM Trans. Program. Lang. Syst., 2019

Intersection types and runtime errors in the pi-calculus.
Proc. ACM Program. Lang., 2019

Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs.
J. Autom. Reason., 2019

On Bisimilarity in Lambda Calculi with Continuous Probabilistic Choice.
Proceedings of the Thirty-Fifth Conference on the Mathematical Foundations of Programming Semantics, 2019

Differential Logical Relations, Part I: The Simply-Typed Case (Long Version).
CoRR, 2019

On the Taylor Expansion of Probabilistic λ-Terms (Long Version).
CoRR, 2019

On the Taylor Expansion of Probabilistic lambda-terms.
Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction, 2019

Type-Based Complexity Analysis of Probabilistic Functional Programs.
Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, 2019

Differential Logical Relations, Part I: The Simply-Typed Case.
Proceedings of the 46th International Colloquium on Automata, Languages, and Programming, 2019

Effectful Normal Form Bisimulation.
Proceedings of the Programming Languages and Systems, 2019

2018
On sharing, memoization, and polynomial time.
Inf. Comput., 2018

On Randomised Strategies in the λ-Calculus (Long Version).
CoRR, 2018

On Intersection Types and Probabilistic Lambda Calculi.
Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, 2018

On Randomised Strategies in the λ-calculus.
Proceedings of the 19th Italian Conference on Theoretical Computer Science, 2018

2017
Automating sized-type inference for complexity analysis.
Proc. ACM Program. Lang., 2017

Encoding Turing Machines into the Deterministic Lambda-Calculus.
CoRR, 2017

The Geometry of Concurrent Interaction: Handling Multiple Ports by Way of Multiple Tokens (Long Version).
CoRR, 2017

Effectful Applicative Bisimilarity: Monads, Relators, and Howe's Method (Long Version).
CoRR, 2017

Probabilistic Termination by Monadic Affine Sized Typing (Long Version).
CoRR, 2017

Metric Reasoning About λ-Terms: The General Case (Long Version).
CoRR, 2017

On Higher-Order Probabilistic Subrecursion (Long Version).
CoRR, 2017

Automating Sized Type Inference for Complexity Analysis (Technical Report).
CoRR, 2017

Automated Sized-Type Inference and Complexity Analysis.
Proceedings of the Proceedings 8th Workshop on Developments in Implicit Computational Complexity and 5th Workshop on Foundational and Practical Aspects of Resource Analysis, 2017

The geometry of parallelism: classical, probabilistic, and quantum effects.
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

The geometry of concurrent interaction: Handling multiple ports by way of multiple tokens.
Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

Effectful applicative bisimilarity: Monads, relators, and Howe's method.
Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

Metric Reasoning About \lambda -Terms: The General Case.
Proceedings of the Programming Languages and Systems, 2017

2016
Light logics and higher-order processes.
Math. Struct. Comput. Sci., 2016

On session types and polynomial time.
Math. Struct. Comput. Sci., 2016

Computation by interaction for space-bounded functional programming.
Inf. Comput., 2016

Higher-order interpretations and program complexity.
Inf. Comput., 2016

Infinitary λ-Calculi from a Linear Perspective (Long Version).
CoRR, 2016

(Leftmost-Outermost) Beta Reduction is Invariant, Indeed.
Log. Methods Comput. Sci., 2016

Infinitary Lambda Calculi from a Linear Perspective.
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

A lambda-calculus foundation for universal probabilistic programming.
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

2015
Developments in Implicit Complexity (DICE 2012).
Theor. Comput. Sci., 2015

A higher-order characterization of probabilistic polynomial time.
Inf. Comput., 2015

Applicative Bisimulation and Quantum λ-Calculi (Long Version).
CoRR, 2015

Parallelism and Synchronization in an Infinitary Context (Long Version).
CoRR, 2015

Metric Reasoning about λ-Terms: the Affine Case (Long Version).
CoRR, 2015

On Equivalences, Metrics, and Polynomial Time (Long Version).
CoRR, 2015

Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order (Long Version).
CoRR, 2015

On Sharing, Memoization, and Polynomial Time (Long Version).
CoRR, 2015

Parallelism and Synchronization in an Infinitary Context.
Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, 2015

Metric Reasoning about λ-Terms: The Affine Case.
Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, 2015

Analysing the complexity of functional programs: higher-order meets first-order.
Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, 2015

Applicative Bisimulation and Quantum λ-Calculi.
Proceedings of the Fundamentals of Software Engineering - 6th International Conference, 2015

On Equivalences, Metrics, and Polynomial Time.
Proceedings of the Fundamentals of Computation Theory - 20th International Symposium, 2015

On Coinduction and Quantum Lambda Calculi.
Proceedings of the 26th International Conference on Concurrency Theory, 2015

On Applicative Similarity, Sequentiality, and Full Abstraction.
Proceedings of the Correct System Design, 2015

2014
Linear dependent types in a call-by-value scenario.
Sci. Comput. Program., 2014

Probabilistic Recursion Theory and Implicit Computational Complexity.
Sci. Ann. Comput. Sci., 2014

Wave-Style Token Machines and Quantum Lambda Calculi.
Proceedings of the Proceedings Third International Workshop on Linearity, 2014

Probabilistic Recursion Theory and Implicit Computational Complexity (Long Version).
CoRR, 2014

The Geometry of Synchronization (Long Version).
CoRR, 2014

On Probabilistic Applicative Bisimulation and Call-by-Value λ-Calculi (Long Version).
CoRR, 2014

Beta Reduction is Invariant, Indeed (Long Version).
CoRR, 2014

On coinductive equivalences for higher-order probabilistic functional programs.
Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

Probabilistic Recursion Theory and Implicit Computational Complexity.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2014, 2014

Measurements in Proof Nets as Higher-Order Quantum Circuits.
Proceedings of the Programming Languages and Systems, 2014

On Probabilistic Applicative Bisimulation and Call-by-Value λ-Calculi.
Proceedings of the Programming Languages and Systems, 2014

The geometry of synchronization.
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2014

Beta reduction is invariant, indeed.
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2014

2013
On Coinductive Equivalences for Higher-Order Probabilistic Functional Programs (Long Version).
CoRR, 2013

Complexity Analysis in Presence of Control Operators and Higher-Order Functions (Long Version).
CoRR, 2013

The geometry of types.
Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

Complexity Analysis in Presence of Control Operators and Higher-Order Functions.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

2012
On quasi-interpretations, blind abstractions and implicit complexity.
Math. Struct. Comput. Sci., 2012

Probabilistic operational semantics for the lambda calculus.
RAIRO Theor. Informatics Appl., 2012

The Geometry of Types (Long Version)
CoRR, 2012

Computational Complexity of Interactive Behaviors
CoRR, 2012

On Constructor Rewrite Systems and the Lambda Calculus
Log. Methods Comput. Sci., 2012

Linear Dependent Types in a Call-by-Value Scenario (Long Version)
CoRR, 2012

An Higher-Order Characterization of Probabilistic Polynomial Time (Long Version)
CoRR, 2012

On the Invariance of the Unitary Cost Model for Head Reduction (Long Version)
CoRR, 2012

On the Invariance of the Unitary Cost Model for Head Reduction.
Proceedings of the 23rd International Conference on Rewriting Techniques and Applications (RTA'12) , 2012

2011
Realizability models and implicit complexity.
Theor. Comput. Sci., 2011

Light logics and optimal reduction: Completeness and complexity.
Inf. Comput., 2011

On Multiplicative Linear Logic, Modality and Quantum Circuits
Proceedings of the Proceedings 8th International Workshop on Quantum Physics and Logic, 2011

Soft Session Types
Proceedings of the Proceedings 18th International Workshop on Expressiveness in Concurrency, 2011

Soft Session Types (Long Version)
CoRR, 2011

Linear Dependent Types and Relative Completeness
Log. Methods Comput. Sci., 2011

A Short Introduction to Implicit Computational Complexity.
Proceedings of the Lectures on Logic and Computation, 2011

2010
Quantum implicit computational complexity.
Theor. Comput. Sci., 2010

A Semantic Proof of Polytime Soundness of Light Affine Logic.
Theory Comput. Syst., 2010

General Ramified Recurrence is Sound for Polynomial Time
Proceedings of the Proceedings International Workshop on Developments in Implicit Computational complExity, 2010

Bounded Linear Logic, Revisited
Log. Methods Comput. Sci., 2010

Functional Programming in Sublinear Space.
Proceedings of the Programming Languages and Systems, 2010

Type Inference for Sublinear Space Functional Programming.
Proceedings of the Programming Languages and Systems - 8th Asian Symposium, 2010

2009
Context semantics, linear logic, and computational complexity.
ACM Trans. Comput. Log., 2009

The geometry of linear higher-order recursion.
ACM Trans. Comput. Log., 2009

On a measurement-free quantum lambda calculus with classical control.
Math. Struct. Comput. Sci., 2009

Confluence Results for a Quantum Lambda Calculus with Measurements.
Proceedings of the 6th International Workshop on Quantum Physics and Logic, 2009

Taming Modal Impredicativity: Superlazy Reduction.
Proceedings of the Logical Foundations of Computer Science, International Symposium, 2009

Derivational Complexity Is an Invariant Cost Model.
Proceedings of the Foundational and Practical Aspects of Resource Analysis, 2009

2008
The weak lambda calculus as a reasonable machine.
Theor. Comput. Sci., 2008

Light Logics and the Call-by-Value Lambda Calculus.
Log. Methods Comput. Sci., 2008

Quantitative Game Semantics for Linear Logic.
Proceedings of the Computer Science Logic, 22nd International Workshop, 2008

2007
Compact and tractable automaton-based representations of time granularities.
Theor. Comput. Sci., 2007

Quantum Lambda Calculi with Classical Control: Syntax and Expressive Power
CoRR, 2007

On the Equivalence of Automaton-Based Representations of Time Granularities.
Proceedings of the 14th International Symposium on Temporal Representation and Reasoning (TIME 2007), 2007

2006
On light logics, uniform encodings and polynomial time.
Math. Struct. Comput. Sci., 2006

An Invariant Cost Model for the Lambda Calculus.
Proceedings of the Logical Approaches to Computational Barriers, 2006

2005
Semantic frameworks for implicit computational complexity.
PhD thesis, 2005

Elementary Affine Logic and the Call-by-Value Lambda Calculus.
Proceedings of the Typed Lambda Calculi and Applications, 7th International Conference, 2005

Quantitative Models and Implicit Complexity.
Proceedings of the FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 2005

2004
Phase semantics and decidability of elementary affine logic.
Theor. Comput. Sci., 2004

2003
Higher-Order Linear Ramified Recurrence.
Proceedings of the Types for Proofs and Programs, International Workshop, 2003

Towards Compact and Tractable Automaten-Based Representations of Time Granularities.
Proceedings of the Theoretical Computer Science, 8th Italian Conference, 2003

On the Expressive Power of Light Affine Logic.
Proceedings of the Theoretical Computer Science, 8th Italian Conference, 2003

2002
Planning with a Language for Extended Goals.
Proceedings of the Eighteenth National Conference on Artificial Intelligence and Fourteenth Conference on Innovative Applications of Artificial Intelligence, July 28, 2002

2001
Calendars, Time Granularities, and Automata.
Proceedings of the Advances in Spatial and Temporal Databases, 7th International Symposium, 2001


  Loading...