Victor Arrial
IRIF, Paris Cité
https://www.irif.fr/users/arrial/index
Date(s) : 04/05/2023 iCal
11 h 00 min - 12 h 30 min
We study the inhabitation problem for a language called 𝜆!, a subsuming paradigm (inspired by call-by-push-value) being able to encode Call-by-Name and Call-by-Value strategies of functional programming. The type specification uses a non-idempotent intersection type system, which is able to capture quantitative properties about the dynamics of programs. Our general methodology can be used to derive inhabitation algorithms for CbN and CbV lambda-calculi.
In the presentation, we detail the tools and explain the method solving this inhabitation problem. We will in particular explore the notion of approximants and their behaviour through the CbN and CbV encodings, the formers being at the core of the completeness of the method. We will also give a general overview of the inhabitation algorithm as well as a few insights on its termination.
https://www.irif.fr/~kesner/papers/popl23.pdf
Emplacement
Amphi 5 - TPR2 (room 500-504, fifth floor)
Catégories