[TYPES] Reference to typed first class pattern matching

[Michael Lienhardt]

Hello,

I was wondering if there was any existing work on typed first class  
pattern matching.

Typically, I have a ML-like calculus with abstraction of the form $ 
\lambda P.e$, were $P$ is a pattern matching for instance type  
constructors and tuples.
Moreover, one can combine abstraction like in $\lambda P.e + \lambda  
P'.e'$, thus assembling pattern matching branches dynamically.
One can also define a function $\lambda g.\lambda f.(f + g)$: we have  
first class pattern matching.

I am interested to type such a calculus, using for instance  
intersection types to deal with the $+$ constructor.
Is there any previous work on first class pattern matching that can  
help me design such a type system ?

Michael Lienhardt
PhD student.