UP - logo
E-resources
Full text
Peer reviewed Open access
  • Quantitative Inhabitation f...
    Arrial, Victor; Guerrieri, Giulio; Kesner, Delia

    Proceedings of ACM on programming languages, 01/2023, Volume: 7, Issue: POPL
    Journal Article

    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 λ!.