Search

• < Previous
• 1
• Next >

Solvability = Typability + Inhabitation

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 inhabitation in an intersection type system P based on non-idempotent types. We show first that the system P characterizes the&nbsp;[&hellip;]