The possibility that the execution of an algorithm may not give rise to a deterministic but rather to a stochastic process has been contemplated since the dawn of theoretical computer science. This idea has had a huge impact on many areas of the theory and practice of computing, e.g., computational complexity and cryptography. But what happens to programs and to their semantics when the former are allowed to evolve probabilistically? The purpose of this course is to introduce students to the challenges the presence of randomisation poses to the design and study of programming languages. After briefly introducing randomisation from a computational viewpoint, we will see how this feature impacts the semantics of programming languages and the task of verifying programs for correctness. We will proceed highlighting when, why, and to which extent the underlying theory diverges from the classic one. While aware of the impossibility of being exhaustive, we will try to provide pointers to the literature whenever it is not possible to go into detail. We will concentrate our attention to functional programming languages as idioms and to type-theoretical verification tools.
De lenguajes de programación determinísticos a randomizados. Cálculos de lambda randomizados. Razonamiento relacional sobre términos Lambda.Semánticas denotacionales. Terminación probabilística y su naturaleza computacional. Sistemas de tipo y elección probabilística. Tópicos avanzados
Se sugiere:
Ser estudiantes avanzados o graduados de computación o matemáticas.
Ugo Dal Lago. On Probabilistic Lambda-Calculi, páginas 121–144. Cambridge University Press,(2020).
Claire Jones and Gordon D. Plotkin. A probabilistic powerdomain of evaluations. In Pro-ceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS 1989), páginas 186–195. IEEE Computer Society, (1989).
Glynn Winskel. The Formal Semantics of Programming Languages. Foundation of computing series. MIT Press, (1993).
Desarrollado por el Departamento de Computación, FCEyN, UBA