37 citations · 96 across the 19 of their papers we have counts for
3 papers · 2 filters
Solvability = Typability + Inhabitation
Antonio Bucciarelli, Delia Kesner, Simona Ronchi Della Rocca
We extend the classical notion of solvability to a lambda-calculus equipped with pattern matching. We prove that solvability can be characterized by means of typability and inhabit…
Non-idempotent types for classical calculi in natural deduction style
Delia Kesner, Pierre Vial
In the first part of this paper, we define two resource aware typing systems for the λμ-calculus based on non-idempotent intersection and union types. The non-idempotent approach p…
Call-by-Need, Neededness and All That
Delia Kesner, Alejandro Ríos, Andrés Viso
We show that call-by-need is observationally equivalent to weak-head needed reduction. The proof of this result uses a semantical argument based on a (non-idempotent) intersection…