[TYPES] Reference to typed first class pattern matching

[Philip Wadler]

Another work that may be relevant is:

   Noam Zeilberger: Focusing and higher-order abstract syntax. POPL  
2008: 359-369

Yours,  -- P

On 10 Sep 2008, at 20:13, eduardo at sol.lifia.info.unlp.edu.ar wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ 
> types-list ]
>
> Dear Micheal,
>
>       There are a number of references that are related to your
> question and that you might find useful (listed in no particular  
> order):
>
>       1) Old (1990) work by Vincent van Oostrom on a lambda calculus
> allowing one to abstract over arbitrary terms ("Lambda calculus with
> patterns"). Untyped setting. [1]
>       2) Previous work revised and extended (joint with Klop and De  
> Vrijer)[2]
>       3) Work by Gilles Barthe et al on PTS with patterns [3]
>       4) Work of Barry Jay on his Bondi programming language (see  
> his homepage)
>       5) Delia Kesner and Barry Jay's First-Class Patterns (see Delia
> Kesner's homepage)
>       6) The rho calculus (see Horatiu Cirstea's homepage)
>
>       Regards,
>       E.
>
>
> [1] Vincent van Oostrom
> Lambda Calculus with Patterns
> Technical Report IR-228, Vrije Universiteit, Amsterdam, 40 pages,
> November 1990
>
> [2] Jan Willem Klop, Vincent van Oostrom, and Roel de Vrijer
> Lambda Calculus with Patterns
> Theoretical Computer Science, Volume 398, Issues 1-3, 28 May 2008,
> pages 16-31, Elsevier
>
> [3] Gilles Barthe, Horatiu Cirstea, Claude Kirchner, Luigi Liquori:
> Pure patterns type systems. POPL 2003: 250-261
>
>
> Quoting Michael Lienhardt <michael.lienhardt at inrialpes.fr>:
>
>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ 
>> types-list ]
>>
>> 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.
>>
>
>
>
> ----------------------------------------------------------------
> Este mensaje ha sido enviado utilizando IMP desde LIFIA.
>


-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.