[TYPES] Reference to typed first class pattern matching

[eduardo@sol.lifia.info.unlp.edu.ar]

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.