May 20 at 3 pm
Doctoral Programme | Computer Science
Defense | A Quantitative Study of Higher-Order Computations with Effects
Student | Jorge Miguel Soares Ramos
Date: May 20
Time: 15:00 pm
Venue: Room FC6 029
President:
António Mário da Silva Marcos Florido
Full Professor
Computer Science Department, Faculty of Sciences, University of Porto
Arguentes:
Ugo Dal Lago
Full Professor
Dipartimento di Informatica - Scienza e Ingegneria, University of Bologna
Danel Ahman
Associate Professor
Institute of Computer Science, University of Tartu
Vogais:
Sabine Babette Broda
Associate Professor
Computer Science Department, Faculty of Sciences, University of Porto
Delia Kesner (Co-orientadora)
Full Professor
UFR d'Informatique, Université Paris Cité
Abstract:
Non-idempotent intersection types have emerged as a powerful logical framework for providing exact quantitative semantics of higher-order programs, allowing typing derivations to capture precise information about resource usage such as evaluation length. While these techniques are now well understood for the pure λ-calculus,extending them to richer language features involving control and computational effects remains a challenging problem.
This thesis develops non-idempotent intersection type systems for extensions of the λ-calculus featuring pattern matching mechanisms and computational effects, with the aim of providing exact, syntax-directed cost semantics grounded in operational semantics. The contributions are organized around two main axes.
The first part of the thesis studies pattern matching as a fundamental extension of the λ calculus. Building on prior quantitative analyses of pattern-matching calculi, we develop refined and generalized non-idempotent intersection type systems that preserve exact correspondence between typing derivations and evaluation length. Particular attention is devoted to the treatment of stuck computations. Exploiting the classical encoding of exceptions via pattern matching, we extend this analysis to exceptional control flow, showing that exception raising and handling admit exact quantitative semantics despite constituting a non-algebraic computational effect.
The second part of the thesis addresses algebraic operations and effects. We focus on algebraic theories that admit non-trivial comodels, which provide a coalgebraic basis for defining fine grained operational semantics via comodel-based transition systems. For calculi with global state, wedefinesuch operational semantics and develop non-idempotent intersection type systems that precisely account for both computational and effectful steps. We then generalize this approach by modeling state as a mapping from locations to infinite stacks, yielding a uniform quantitative framework capable of capturing abroad class of algebraic effects, including globalstate, interactive input/output, and finite nondeterminism.
Throughout the thesis, the λ!-calculus plays a unifying role, subsuming call-by-name and call-by-value evaluation strategies while retaining the operational granularity required for exact quantitative reasoning. Overall, this work significantly extends the scope of non-idempotent inter section types, demonstrating their applicability to languages with pattern matching, exceptions, and algebraic effects, and providing a unified operational and quantitative account of resource sensitive computation