May 25th, at 14:30, Room FC6 1.40 (S2), Department of Computer Science, FCUP
Please register: https://forms.gle/DGNxvmTmYXgKFijV7
Abstract
Moving from the abstract definition of monads, we introduce a version of the call-by-value computational λ-calculus based on Wadler’s variant. We call the calculus computational core and study its reduction, prove it confluent, and study its operational properties on two crucial properties: returning a value and having a normal form. The cornerstone of our analysis is factorization results.
In the second part, we study a Curry style type assignment system for the computational core. We introduce an intersection type system inspired by Barendregt, Coppo, and Dezani system for ordinary untyped λ-calculus, establishing type invariance under conversion. Finally, we introduce a notion of convergence, which is precisely related to reduction, and characterize convergent terms via their types.
In the conclusion, we give an overview of the computational core extended with operators representing read and write operations from and to a global store.
Short biography
Riccardo Treglia has a post-doctoral position at the Department of Computer Science at the University of Bologna. He obtained a Ph.D. degree in Computer Science from the University of Turin in 2022, under the supervision of Ugo de'Liguoro. Specifically, he studies lambda-calculus, intersection types, and rewriting theory with a particular interest in monadic frameworks.
About Talks@DCC :
The mission of the Talks@DCC seminars is to bring together researchers and students, to foster discussions and promote scientific awareness and collaboration. Participate: attend and propose your talk.