[ Home | Research | Teaching ]

I shall be sorry if computer science ever
flies apart into two disciplines, one logical
and one technological. -- Robin Milner.

Currently, my research interests are the following: In the past, I also worked on: Papers and Publications

Journals
[MSCS2016] Ugo Dal Lago, Simone Martini, and Davide Sangiorgi. Light Logics and Higher-Order Processes. Mathematical Structures in Computer Science, 26(6):962-992, 2016. [ doi ]
[LMCS2016] Beniamino Accattoli, and Ugo Dal Lago. (Leftmost-Outermost) Beta Reduction is Invariant, Indeed. Logical Methods in Computer Science, 12(1), 2016. [ doi ]
[I&C2016b] Ugo Dal Lago, and Ulrich Schoepp. Computation by Interaction for Space-Bounded Functional Programming Information and Computation, 248:150-194, 2016. [ doi ]
[I&C2016b] Ugo Dal Lago, and Patrick Baillot. Higher-order Interpretations and Program Complexity Information and Computation, 248:56-81, 2016. [ doi ]
[I&C2015] Ugo Dal Lago, and Paolo Parisen Toldin. A Higher-Order Characterization of Probabilistic Polynomial Time. Information and Computation, 241:114-141, 2015. [ doi ]
[SACS2014] Ugo Dal Lago, Sara Zuppiroli, and Maurizio Gabbrielli. Probabilistic Recursion Theory and Implicit Computational Complexity. Scientific Annals of Computer Science, 44:177-216, 2014. [ doi ]
[SCP2014] Ugo Dal Lago, and Barbara Petit. Linear Dependent Types in a Call-by-Value Scenario. Science of Computer Programming, 84:77-100, 2012. [ doi ]
[LMCS2012a] Ugo Dal Lago, and Simone Martini. On Constructor Rewrite Systems and the Lambda Calculus. Logical Methods in Computer Science, 8(3), 2012. [ doi ]
[LMCS2012b] Ugo Dal Lago, and Marco Gaboardi. Linear Dependent Types and Relative Completeness. Logical Methods in Computer Science, 8(4), 2012. [ doi ]
[MSCS2012] Patrick Baillot, Ugo Dal Lago, and Jean-Yves Moyen. On quasi-interpretations, blind abstractions and implicit complexity. Mathematical Structures in Computer Science, 22(4):249-280, 2012. [ doi ]
[RAIRO2012] Ugo Dal Lago, Margherita Zorzi. Probabilistic Operational Semantics for the Lambda Calculus. RAIRO - Theoretical Informatics and Applications, 46(3):413-450, 2012. [ doi ]
[ENTCS2011] Ugo Dal Lago, Andrea Masini, Margherita Zorzi. Confluence Results for a Quantum Lambda Calculus with Measurements. Electronic Notes on Theoretical Computer Science, 270(2):251-261, 2011. [ doi ]
[I&C2011] Patrick Baillot, Paolo Coppola, Ugo Dal Lago. Light logics and optimal reduction: Completeness and complexity. Information and Computation, 209(2):118-142, 2011. [ doi ]
[TCS2011] Ugo Dal Lago and Martin Hofmann. Realizability Models and Implicit Complexity. Theoretical Computer Science, 412(20):2029-2047, 2011. [ doi ]
[LMCS2010] Ugo Dal Lago and Martin Hofmann. Bounded Linear Logic, Revisited. Logical Methods in Computer Science, 6(4), 2010. [ doi ]
[TOCS2010] Ugo Dal Lago and Martin Hofmann. A semantic proof of polytime soundness for light affine logic. Theory of Computing Systems, 46(4), 2010. [ doi ]
[TCS2010] Ugo Dal Lago, Andrea Masini, and Margherita Zorzi. Quantum implicit computational complexity. Theoretical Computer Science, 411(2), 2010. [ doi ]
[TOCL2009a] Ugo Dal Lago. The geometry of linear higher-order recursion. ACM Transactions on Computational Logic, 10(2), 2009. [ doi ] [ arxiv ]
[TOCL2009b] Ugo Dal Lago. Context semantics, linear logic and computational complexity. ACM Transactions on Computational Logic, 10(4), 2009. [ doi ] [ arxiv ]
[MSCS2009] Ugo Dal Lago, Andrea Masini, and Margherita Zorzi. On a measurement-free quantum lambda calculus with classical control. Mathematical Structures in Computer Science, 19(2):297-335, 2009. [ doi ] [ arxiv ]
[LMCS2008] Paolo Coppola, Ugo Dal Lago, and Simonetta Ronchi Della Rocca. Light logics and the call-by-value lambda calculus. Logical Methods in Computer Science, 4(4), 2008. [ doi ] [ arxiv ]
[TCS2008] Ugo Dal Lago and Simone Martini. The weak lambda-calculus as a reasonable machine. Theoretical Computer Science, 398(1-3):32-50, 2008. [ doi ]
[TCS2007] Ugo Dal Lago, Angelo Montanari, and Gabriele Puppis. Compact and tractable automaton-based representations of time granularities. Theoretical Computer Science, 373(1-2):115-141, 2007. [ doi ]
[MSCS2006] Ugo Dal Lago and Patrick Baillot. On light logics, uniform encodings and polynomial time. Mathematical Structures in Computer Science, 16(4):713-733, 2006. [ doi ]
[TCS2004] Ugo Dal Lago and Simone Martini. Phase semantics and decidability of elementary affine logic. Theoretical Computer Science, 318(3):409-433, 2004. [ doi ]
Conferences
[FCT2015] Alberto Cappai, and Ugo Dal Lago. On Equivalences, Metrics, and Polynomial Time. In 20th International Symposium on Fundamentals of Computation Theory, Proceedings, pages 311-323. 2015. [ doi ]
[CONCUR2015] Yuxin Deng, Yuan Feng, and Ugo Dal Lago. On Coinduction and Quantum Lambda Calculi. In 26th International Conference on Concurrency Theory, Proceedings, pages 427-440. 2015. [ doi ]
[LICS2015a] Raphaëlle Crubillé, and Ugo Dal Lago. Metric Reasoning about λ-Terms: The Affine Case. In 32th Annual IEEE/ACM Symposium on Logic in Computer Science, Proceedings, pages 633-644. 2015. [ doi ]
[LICS2015b] Ugo Dal Lago, Claudia Faggian, Benoit Valiron, and Akira Yoshimizu. Parallelism and Synchronization in an Infinitary Context.. In 32th Annual IEEE/ACM Symposium on Logic in Computer Science, Proceedings, pages 559-572. 2015. [ doi ]
[LPAR2015] Patrick Baillot, Gilles Barthe, and Ugo Dal Lago. Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs. In 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Proceedings, volume 9450 of Lecture Notes in Computer Science, pages 203-218. 2015. [ doi ]
[STACS2015] Martin Avanzini, and Ugo Dal Lago. On Sharing, Memoization, and Polynomial Time. In 32nd International Symposium on Theoretical Aspects of Computer Science, Proceedings, volume 30 of Leibniz International Proceedings in Informatics, pages 62-75. 2015. [ doi ]
[LINEARITY2014] Ugo Dal Lago, and Margherita Zorzi. Wave-Style Token Machines and Quantum Lambda Calculi. In Third International Workshop on Linearity, Proceedings, volume 176 of Electronic Proceedings on Theoretical Computer Secience, pages 64-78. 2015. [ doi ]
[ICTAC2014] Ugo Dal Lago, and Sara Zuppiroli. Probabilistic Recursion Theory and Implicit Computational Complexity. In Theoretical Aspects of Computing, Eleventh International Colloquium, Proceedings, volume 8687 of Lecture Notes in Computer Science , pages 97-114. 2014. [ doi ]
[CSLLICS2014b] Ugo Dal Lago, Claudia Faggian, Ichiro Hasuo, Akira Yoshimizu. The Geometry of Synchronization. In Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic, and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science, Proceedings, pages 35:1-35:10. 2014. [ doi ]
[CSLLICS2014a] Beniamino Accattoli, and Ugo Dal Lago. Beta reduction is invariant, indeed. In Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic, and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science, Proceedings, pages 8:1-8:10. 2014. [ doi ]
[ESOP2014a] Raphaëlle Crubillé, and Ugo Dal Lago. On Probabilistic Applicative Bisimulation and Call-by-Value Lambda-Calculi. In Programming Languages and Systems, 23rd European Symposium on Programming, Proceedings, volume 8410 of Lecture Notes in Computer Science, pages 209-228. Springer, 2014. [ doi ]
[ESOP2014b] Akira Yoshimitzu, Ichiro Hasuo, Claudia Faggian, and Ugo Dal Lago. Measurements in Proof Nets as Higher-Order Quantum Circuits. In Programming Languages and Systems, 23rd European Symposium on Programming, Proceedings, volume 8410 of Lecture Notes in Computer Science, pages 371-391. Springer, 2014. [ doi ]
[POPL2014] Ugo Dal Lago, Davide Sangiorgi, and Michele Alberti. On Coinductive Equivalences for Higher-Order Probabilistic Functional Programs. In 41st International Symposium on Principles of Programming Languages, Proceedings, pages 297-308. 2014. [ doi ]
[LPAR2013] Ugo Dal Lago and Giulio Pellitta. Complexity Analysis in Presence of Control Operators and Higher-Order Functions. In 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Proceedings, pages 258-267. 2013. [ doi ]
[POPL2013] Ugo Dal Lago and Barbara Petit. The Geometry of Types. In 40th International Symposium on Principles of Programming Languages, Proceedings, pages 167-178. 2013. [ doi ]
[CSL2012] Patrick Baillot and Ugo Dal Lago. Higher-Order Interpretations and Program Complexity In 21st International Conference of the EACSL, Proceedings, volume 16 of Leibniz International Proceedings in Informatics, pages 62-76. 2012. [ doi ]
[PPDP2012] Ugo Dal Lago and Barbara Petit. Linear Dependent Types in a Call-by-Value Scenario In 14th International Symposium on Principles and Practice of Declarative Programming, Proceedings, ACM Press, pages 115-126. 2012. [ doi ]
[RTA2012] Beniamino Accattoli and Ugo Dal Lago. On the Invariance of the Unitary Cost Model for Head Reduction. In 23rd International Conference on Rewriting Techniques and Applications, Proceedings, volume 15 of Leibniz International Proceedings in Informatics, pages 55-66. 2012. [ doi ]
[QPL2011] Ugo Dal Lago and Claudia Faggian. On Multiplicative Linear Logic, Modality and Quantum Circuits. In 8th International Workshop on Quantum Physics and Logic, Proceedings, volume 95 of Electronic Proceedings on Theoretical Computer Science, pages 55-66. 2011. [ doi ]
[EXPRESS2011] Ugo Dal Lago and Paolo Di Giamberardino. Soft Session Types. In 18th International Workshop on Expressiveness in Concurrency, Proceedings, volume 64 of Electronic Proceedings on Theoretical Computer Science, pages 59-73. 2011. [ doi ]
[LICS2011] Ugo Dal Lago and Marco Gaboardi. Linear Dependent Types and Relative Completeness. In Logic in Computer Science, 26th International Symposium, Proceedings, pages 133-142. IEEE Computer Society, 2011. [ doi ] [ arxiv ]
[APLAS2010] Ugo Dal Lago and Ulrich Schoepp. Type Inference for Sublinear Space Functional Programming. In Programming Languages and Systems - 8th Asian Symposium, Proceedings, volume 6461 of Lecture Notes in Computer Science, pages 376-391. Springer, 2010. [ doi ]
[EXPRESS2010] Ugo Dal Lago, Simone Martini and Davide Sangiorgi. Light Logics and Higher-Order Processes. In 17th International Workshop on Expressiveness in Concurrency, Proceedings, volume 41 of Electronic Proceedings on Theoretical Computer Science, pages 46-60. 2010. [ doi ]
[DICE2010] Ugo Dal Lago, Simone Martini and Margherita Zorzi. General Ramified Recurrence is Sound for Polynomial Time. In International Workshop on Developments in Implicit Computational Complexity, Proceedings, volume 23 of Electronic Proceedings on Theoretical Computer Science, pages 47-62. 2010. [ doi ]
[ESOP2010] Ugo Dal Lago and Ulrich Schoepp. Functional Programming in Sublinear Space. In Programming Languages and Systems, 19th European Symposium on Programming, Proceedings, volume 6012 of Lecture Notes in Computer Science, pages 205-225. Springer, 2010. [ doi ]
[ICALP2009] Ugo Dal Lago and Simone Martini. On constructor rewrite systems and the lambda-calculus. In International Conference on Automata, Languages and Programming, Proceedings, volume 5556 of Lecture Notes in Computer Science, pages 163-174. Springer, 2009. [ doi ] [ arxiv ]
[TLCA2009] Ugo Dal Lago and Martin Hofmann. Bounded linear logic, revisited. In Typed Lambda Calculi and Applications, 9th International Conference, Proceedings, volume 5608 of Lecture Notes in Computer Science, pages 80-94. Springer, 2009. [ doi ] [ arxiv ]
[LFCS2009] Ugo Dal Lago, Luca Roversi, and Luca Vercelli. Taming modal impredicativity: Superlazy reduction. In Logical Foundations of Computer Science, International Symposium, Proceedings, volume 5407 of Lecture Notes in Computer Science, pages 137-151. Springer, 2009. [ doi ] [ arxiv ]
[CSL2008] Ugo Dal Lago and Olivier Laurent. Quantitative game semantics for linear logic. In Computer Science Logic, 22nd International Workshop, Proceedings, volume 5213 of Lecture Notes in Computer Science, pages 230-245. Springer, 2008. [ doi ] [ hal ]
[CSR2008] Ugo Dal Lago and Martin Hofmann. A semantic proof of polytime soundness of light affine logic. In Third International Computer Science Symposium in Russia, Proceedings, volume 5010 of Lecture Notes in Computer Science, pages 134-145. Springer, 2008. [ doi ]
[LICS2007] Patrick Baillot, Paolo Coppola, and Ugo Dal Lago. Light logics and optimal reduction: Completeness and complexity. In Logic in Computer Science, 22nd International Symposium, Proceedings, pages 421-430. IEEE Computer Society, 2007. [ doi ] [ arxiv ]
[TIME2007] Ugo Dal Lago, Angelo Montanari, and Gabriele Puppis. On the equivalence of automaton-based representations of time granularities. In 14th International Symposium on Temporal Representation and Reasoning, Proceedings, pages 82-93. IEEE Computer Society, 2007. [ doi ]
[LICS2006] Ugo Dal Lago. Context semantics, linear logic and computational complexity. In Logic in Computer Science, 20th International Symposium, Proceedings, pages 169-178. IEEE Computer Society, 2006. [ doi ] [ arxiv ]
[CIE2006] Ugo Dal Lago and Simone Martini. An invariant cost model for the lambda calculus. In Arnold Beckmann, Ulrich Berger, Benedikt Loewe, and John V. Tucker, editors, Logical Approaches to Computational Barriers, Second Conference on Computability in Europe, CiE 2006, Proceedings, volume 3988 of Lecture Notes in Computer Science, pages 105-114. Springer, 2006. [ doi ] [ arxiv ]
[FSTTCS2005] Ugo Dal Lago and Martin Hofmann. Quantitative models and implicit complexity. In R. Ramanujam and Sandeep Sen, editors, Foundations of Software Technology and Theoretical Computer Science, Proceedings, volume 3821 of Lecture Notes in Computer Science, pages 189-200. Springer, 2005. [ doi ] [ arxiv ]
[LICS2005] Ugo Dal Lago. The geometry of linear higher-order recursion. In Logic in Computer Science, 20th International Symposium, Proceedings, pages 366-375. IEEE Computer Society, 2005. [ doi ] [ arxiv ]
[TLCA2005] Paolo Coppola, Ugo Dal Lago, and Simona Ronchi Della Rocca. Elementary affine logic and the call-by-value lambda calculus. In Pawel Urzyczyn, editor, Typed Lambda Calculi and Applications, 7th International Conference, Proceedings, volume 3461 of Lecture Notes in Computer Science, pages 131-145. Springer, 2005. [ doi ]
[TYPES2003] Ugo Dal Lago, Simone Martini, and Luca Roversi. Higher order linear ramified recurrence. In Types for Proofs and Programs, Post-Workshop Proceedings, volume 3085 of Lecture Notes in Computer Science, pages 178-193. Springer, 2003. [ doi ]
[ICTCS2003a] Ugo Dal Lago. On the expressive power of light affine logic. In Carlo Blundo and Cosimo Laneve, editors, Eight Italian Conference on Theoretical Computer Science, Proceedings, volume 2841 of Lecture Notes in Computer Science, pages 216-227. Springer, 2003. [ doi ]
[ICTCS2003b] Ugo Dal Lago, Angelo Montanari, and Gabriele Puppis. Towards a compact and tractable automaton-based representations of time granularities. In Carlo Blundo and Cosimo Laneve, editors, Eight Italian Conference on Theoretical Computer Science, Proceedings, volume 2841 of Lecture Notes in Computer Science, pages 72-85. Springer, 2003. [ doi ]
[AAAI2002] Ugo Dal Lago, Marco Pistore, and Paolo Traverso. Planning with a language for extended goals. In Eighteenth National Conference of Artificial Intelligence, Proceedings, pages 447-454. AAAI Press, 2002.
[SSTD2001] Ugo Dal Lago and Angelo Montanari. Calendars, time granularities and automata. In Christian S. Jensen, Markus Schneider, Bernhard Seeger, and Vassilis J. Tsotras, editors, Advances in Spatial and Temporal Databases, 7th International Symposium, Proceedings, volume 2121 of Lecture Notes in Computer Science, pages 279-298. Springer, 2001. [ doi ]
Book Chapters
[ESSLLI2010] Ugo Dal Lago. A Short Introduction to Implicit Computational Complexity. Lectures on Logic and Computation, volume 7388 of Lecture Notes in Computer Science, pages 89-109. Springer, 2011.
[DCE2008] Ugo Dal Lago and Simone Martini. Proofs as efficient programs. In Giovanna Corsi and Rossella Lupacchini, editors, Deduction, Computation, Experiment, pages 141-157. Springer, 2008.
Other
[PDDL2003] Piergiorgio Bertoli, Alessandro Cimatti, Ugo Dal Lago, and Marco Pistore. Extending PDDL to nondeterminism, limited sensing and iterative conditional plans. In ICAPS Workshop on PDDL, Informal Proceedings, pages 15-24, 2003.