Vous pouvez vous abonner à nos annonces de séminaires
                     http://gallium.inria.fr/seminaires/

                             S E M I N A I R E
       __                                  
      / _`  _   /  /  o                       /| /|   __  __  __ __    _  _
     /   ) __) /  /  / /  / /\/|    -----    / |/ |  /  )(_  /  /  ) ) ) __)
    (___/ (_/ (_ (_ / (__/ /   |            /     | (__/ __)(_ (__/ (_/ (_/
                                                
                          I N R I A - Rocquencourt
                        Amphi Turing du bâtiment 1

                        MERCREDI 20 novembre, 10h30

                               -------------
                               Justin Slepak
                               -------------

                          Northeastern University

    ===================================================================
    Array computation and statically typing shape-polymorphic languages
    ===================================================================

Iverson pioneered the development of the shape-polymorphic languages APL and J
for programming array computations. These languages -- for which he received
the Turing award -- are elegant and compact, principally because their control
structure is based on automatically "lifting" lower-dimensional operators for
higher-dimensional operands. In APL and J, the "iteration space" described by
the loop nests of FORTRAN programs is reified in data space as the higher
dimensions of the data arrays; operators then lift across the iteration axes
of these arrays. This means APL and J programs typically have no explicit
loops or recursions.

However, these languages have lacked a static semantics that could be used to
reason about the program at compile time, which has been a long-time barrier
to static debugging and high-performance compilation. I have designed a type
system for a core language that captures and extends Iverson's computational
model. While the type system uses dependent types, it is sufficiently
constrained that type checking is decidable. In addition to the standard
benefits of static typing (e.g., guaranteeing the absence of errors), the
implicit control structure of an array program is made explicit in its type
derivation. My language and its static semantics also eliminate some of the ad
hoc semantic elements Iverson bolted onto his core language. I am currently
working on the problem of how to infer types for this language from a less
heavily annotated surface language.

I will introduce the programming model, with examples; present the core
language and a formal dynamic semantics; then describe the static type system;
and close with a short discussion of the type-inference problem. (And at this
point, in particular, all suggestions and advice would be very welcome.)