About Randomized Programming and Rewriting
14th International School on Rewriting, Obergurgl, Austria
August 2024
Rewriting can be seen as an abstraction of the computational process in which the underlying configuration evolves through the process of substitution of expressions by expressions. As such, rewriting allows you to capture the fundamental concepts of program and algorithm. The latter, however, does not always enjoy a crucial property usually taken for granted, namely that of being deterministic. Indeed, many modern algorithms essentially rely on the availability of true randomness. How could one nicely express randomized algorithms? Would it be possible to capture this new computing paradigm in rewriting? What impact does all this have on the underlying theory? This course aims to provide an introduction to randomized computation, programming and rewriting, while answering the questions above.

Course Program
Schedule
References

[1] Martin Avanzini, Ugo Dal Lago, Akihisa Yamada, On Probabilistic Term Rewriting, Science of Computer Programming, Volume 185, 2020. [pdf]
[2] Ugo Dal Lago, On Probabilistic Lambda Calculi, In: Gilles Barthe, Joost-Pieter Katoen, Alexandra Silva, eds. Foundations of Probabilistic Programming. Cambridge University Press; 2020:121-144. [pdf]
[3] Ugo Dal Lago, Claudia Faggian, Simona Ronchi Della Rocca Intersection Types and (positive) Almost-Sure Termination, Proceedings of the ACM on Programming Languages, Volume 5, Issue POPL Article No.: 32, Pages 1 - 32 [ pdf ]
[4] Ugo Dal Lago, Charles Grellois Probabilistic Termination by Monadic Affine Sized Typing, ACM Transactions on Programming Languages and Systems. [ pdf ]