Mini-workshop on effects and cost models
For the Huawei – University of Edinburgh Tech Talk Series, we are organizing a mini-workshop, in person and online, about foundations of programming languages. There are no registration fees. The details of the program and talks are below. A lunch will be provided between the talks.
When: Tuesday 26 July 2022, from 11:00 to 14:15. (UK time).
Where (in person): Room G.03, Bayes Centre (47 Potterrow, Edinburgh EH8 9BT).
Where (virtually): Zhumu link (https://meeting.zhumu.me/wc/0184220908/join?track_id=&jmf_code=&meeting_result=&tk=&cap=d7cec&prefer=0), everybody is welcome! You can access it from your own browser or Zoom app, without installing anything.
- 10:00-11:00 Coffee and networking / discussions
- 11:00-11:45. Ugo Dal Lago: From Equivalences to Metrics, Effectfully.
- 11:45-12:45. Alexys Ghyselen: On Reinforcement Learning, Effect Handlers, and the State Monad.
- 12:45-13:30. Lunch
- 13:30-14:15. Beniamino Accattoli: Reasonable Space and the Lambda Calculus.
- 14:15-14:30. Coffee
The details of the talks are below.
Speaker: Prof. Ugo Dal Lago (University of Bologna, Italy).
Title: From Equivalences to Metrics, Effectfully.
Abstract: Semantics is traditionally concerned with program equivalence, in which all pairs of programs which are not equivalent are treated the same, and simply dubbed as incomparable. In recent years, various forms of program metrics have been introduced such that the distance between non-equivalent programs is measured as an element of an appropriate quantale. By letting the underlying quantale vary as the type of the compared programs become more complex, the recently introduced framework of differential logical relations allows for a new contextual form of reasoning. We illustrate how all this can be generalised to effectful higher-order programs, in which not only the values, but also the effects computations produce can be appropriately distanced in a principled way. We show that the resulting framework is flexible, allowing various forms of effects to be handled, at the same time providing informative judgments about program differences.
Brief speaker bio: Ugo Dal Lago has been a faculty member of the Computer Science Lab at the University of Bologna since 2006. Before that, he spent a few years as a postdoc between Verona and Paris. His main research interests are the theory of programming languages, quantum computing, and implicit computational complexity. Currently, he is the principal investigator of the ERC CoG project “Differential Program Semantics”, and he is a member of the INRIA EPI “FoCUS”. He co-authored more than 100 publications which appeared in journals and conference proceedings. He is the winner of the prize for the best italian doctoral thesis in theoretical computer science (2006), of the Kleene Award (2006) and of the prize for the best young researcher in theoretical computer science (2015).
Speaker: Dr. Alexis Ghyselen (University of Bologna, Italy).
Title: On Reinforcement Learning, Effect Handlers, and the State Monad.
Abstract: We study algebraic effects and handlers as a way to support decision-making abstractions in functional programs, whereas a user can ask a learning algorithm to resolve choices without implementing the underlying selection mechanism, and give a feedback by way of rewards. Differently from the recently proposed approach to the problem based on the selection monad by Abadi and Plotkin, we express the underlying intelligence as a reinforcement learning algorithm implemented as a set of handlers for some of these algebraic operations, including those for choices and rewards. We show how we can in practice, in the language EFF whose main features are algebraic effects and handlers, clearly separate the learning algorithm from its environment, thus allowing for a good level of modularity. We then show how the host language could be taken as a lambda-calculus with handlers, this way highlighting the essential linguistic features. We conclude by hinting at how type and effect systems could ensure safety properties, at the same time pointing at some directions for further work.
Brief speaker bio: Alexis Ghyselen is a post-doc within the DIAPASoN project since October 2021. He obtained his PhD at ENS Lyon (France), on type-directed complexity analysis in probabilistic functional languages and parallel languages. Overall, he is mainly interested in types, logic and programming languages.
Speaker: Dr. Beniamino Accattoli (Inria & Ecole Polytechnique, France).
Title: Reasonable Space and the Lambda Calculus.
Abstract: The lambda calculus is an expressive mathematical formalism that elegantly captures the core of functional programming languages. The evaluation of programs is modeled as a symbolic rewriting system far from low-level implementative details. This aspect has the drawback that it is not clear how to measure the time and space complexity of functional programs in a reasonable way, that is, in a way that agrees with standard computational complexity. The talk focuses on reasonable space for the lambda calculus, about which—until very recently—almost nothing was known. The talk shall survey recent results in collaboration with Ugo Dal Lago and Gabriele Vanoni (appeared in POPL 2021, LICS 2021, LICS 2022, and ICFP 2022) which have clarified the topic, and led to the first reasonable space cost model for the lambda calculus able to account for logarithmic space.
Brief speaker bio: Beniamino Accattoli obtained his PhD at ‘La Sapienza’ University in Rome (Italy) in 2011, and he is now researcher at Inria & Ecole Polytechnique (France). His work is about the foundation of functional programming languages and proof assistants, using a combination of tools from logic, rewriting theory, and complexity theory. His most relevant contribution, in collaboration with Ugo Dal Lago, is that the lambda calculus can be used as a reasonable model for computational complexity.