Quantitative inhabitation for different lambda calculi in a unifying framework
Date(s) : 04/05/2023 iCal
11h00 - 12h30
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[su_spacer size= »10″]
Emplacement
I2M Luminy - Ancienne BU, Salle Séminaire2 (RdC)
Catégories
