We solve the inhabitation problem for a language called λ!, a subsuming paradigm (inspired by call-by-push-value) being able to encode, among others, 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. As an application, we show how our general methodology can be used to derive inhabitation algorithms for different lambda-calculi that are encodable into λ!.
No takes yet. Share an insight, caveat, or question.
Arrial et al. (2023) studied this question.
Synapse has enriched 5 closely related papers on similar clinical questions. Consider them for comparative context: