TYPES small workshop on Effects and Type Theory

TYPES small workshop on Effects and Type Theory

[Tarmo Uustalu]

In the frame of the extended EU FP6-funded TYPES project, we are
organizing an ad hoc "small workshop" on integration of effects into
type-theoretic programming/reasoning.

This is an informal event and attendance is not confined to people
involved in TYPES. On the contrary, attendance and contributions from
outside the TYPES consortium are most welcome. The invited speakers
are Paul Levy and Aleksandar Nanevski.


---

              Call for contibutions and participation

            Workshop on Effects and Type Theory,  EffTT
               Tallinn, Estonia, 13-14 December 2007

                       http://cs.ioc.ee/efftt/

              a "small workshop" of the TYPES project


Background

The syntax and semantics of impurities of computation known as effects
have been an important challenge for functional programming. Today, we
tend to employ categorically inspired tools such as monads, Lavwere
theories and arrows, but also more pragmatic approaches such as
uniqueness typing.

Effects are an issue also for type-theoretic programming and
reasoning, where a number of aspects make them specifically
interesting. First, we do not yet know what the best dependently typed
generalizations of our simply typed tools are, although we hope they
would reinforce the dual utility of type-theoretic calculi as
programming languages and logics. Second, this duality specifically
forces that pure computations must terminate, so even nontermination
is an impurity and potentially an effect. Third, is it not likely that
the type-theoretic glasses can help us see more clearly the
particularities of external-world effects such as true destructively
updatable state and true interactive input-output?

Thus, this workshop is exactly about effects and type theory. Topics
of interest include

    * all kinds of dependent generalizations of monads and more
    * type-theoretic language design for effects
    * type-theoretic effectful programming methodology
    * time, nontermination and type theory
    * state and type theory,
           including combinations of Hoare-like logics and type theory
    * interactive input-output and type theory
    * theories of external-world effects
    * type theory and concurrency
    * type-theoretic descriptions of physical systems
    * and any further topics about effects and type theory

Invited speakers

Our invited speakers are Paul Levy (Birmingham) and Aleksandar
Nanevski (Microsoft Research, Cambridge).


Contributing a talk

The rest of the programme will be based on contributed talks and
discussions. If you would like to contribute a talk, send a title and
abstract to efftt(at)cs.ioc.ee by 21 November 2007.


Organizers

The workshop organizers are Thorsten Altenkirch, Marino Miculan and
Tarmo Uustalu.


Venue

The workshop will take place in the building of the Estonian Academy
of Sciences on Tallinn's Dome Hill.

The workshop dates are during the Tallinn Christmas market and the
Christmas Jazz festival of Jazzkaar.


Participating

To register, please drop an email to efftt(at)cs.ioc.ee as soon as
possible, but not later than 21 November 2007.

Attendance is not confined to people involved in the TYPES project;
the workshop is open to anyone interested.