Polytypic Programming talk at BU


Subject: Polytypic Programming talk at BU
From: Karl Lieberherr (lieber@ccs.neu.edu)
Date: Fri Apr 20 2001 - 15:44:43 EDT


>From: Torben Amtoft <tamtoft@cs.bu.edu>
>To: Announce Church <church-announce@types.bu.edu>
>Cc: patrikj@cs.chalmers.se
>Subject: Church seminar, Mon Apr 23 at 10am: Patrik Jansson
>
> We have the pleasure of resuming our seminar:
>
>Speaker: Patrik Jansson
> (visiting Northeastern from Chalmers, Sweden, until the end of May)
> http://www.cs.chalmers.se/~patrikj/
>
>Title: Functional Polytypic Programming
>
>Time: Monday, April 23, 2001, 10am to noon
>
>Place: BU, MCS 135 (for directions, see
> http://www.cs.bu.edu/colloquium/ or
> http://types.bu.edu/directions.html)
>
>[This will be a top level overview of the speaker's thesis, the
>abstract of which is given below. Roughly the first half of the talk
>will be spent on polytypic programming in general; the second half of
>the talk will focus on the rewriting application.]
>
>Abstract:
> Many algorithms have to be implemented over and over again for
> different datatypes, either because datatypes change during the
> development of programs, or because the same algorithm is used for
> different datatypes, either because datatypes change during the
> development of programs, or because the same algorithm is used for
> several datatypes. Examples of such algorithms are equality tests,
> pretty printers, and pattern matchers, and polytypic programming is
> a paradigm for expressing such algorithms. This dissertation
> introduces polytypic programming for functional programming
> languages, shows how to construct and prove properties of polytypic
> algorithms, presents the language extension PolyP for implementing
> polytypic algorithms in a type safe way, and presents a number of
> applications of polytypic programming. The applications include a
> library of basic polytypic building blocks, PolyLib, and two larger
> applications of polytypic programming: rewriting and data
> conversion.
>
> PolyP extends a functional language (a subset of Haskell) with a
> construct for defining polytypic functions by induction on the
> structure of user-defined datatypes. Programs in the extended
> language are translated to Haskell.
>
> PolyLib contains powerful structured recursion operators like
> catamorphisms, maps and traversals, as well as polytypic versions of
> a number of standard functions from functional programming: sum,
> length, zip, (==), (&lt;=), etc. Both the specification of the library
> and a PolyP implementation are presented.
>
> The first larger application is a framework for polytypic
> programming on terms. We show that an interface of four functions
> is sufficient to express polytypic functions for pattern matching,
> unification and term rewriting. Using this framework, a term
> rewriting function is specified and transformed into an efficient
> and correct implementation.
>
> In the second application, a number of functions for polytypic data
> conversion are implemented and proved correct. The conversions
> considered include pretty printing, parsing, packing and unpacking
> of structured data. The conversion functions are expressed in an
> embedded domain specific language for data conversion (a hierarchy
> of Haskell's constructor classes).
>



This archive was generated by hypermail 2b28 : Fri Apr 20 2001 - 15:45:25 EDT