CALL FOR PAPERS -- JOURNAL OF FUNCTIONAL PROGRAMMING

[Simon Helsen]

                                CALL FOR PAPERS
                                 SPECIAL ISSUE
                       JOURNAL OF FUNCTIONAL PROGRAMMING:
                DEPENDENT TYPE THEORY MEETS PROGRAMMING PRACTICE

Modern programming languages rely on advanced type systems that detect
errors at compile-time. While the benefits of type systems have long been
recognized, there are some areas where the standard systems in programming
languages are not expressive enough. Language designers usually trade
expressiveness for decidability of the type system. Some interesting
programs will always be rejected (despite their semantical soundness) or
be assigned uninformative types.

There are several remedies to this situation. Dependent type systems,
which allow the formation of types that explicitly depend on other types
or values, are one of the most promising approaches. These systems are
well-investigated from a theoretical point of view by logicians and type
theorists. For example, dependent types are used in proof assistants to
implement various logics and there are sophisticated proof editors for
developing programs in a dependently typed language.

To the present day, the impact of these developments on practical
programming has been small, partially because of the level of
sophistication of these systems and of their type checkers. Only recently,
there have been efforts to integrate dependent systems into intermediate
languages in compilers and programming languages. Additional uses have
been identified in high-profile applications such as mobile code security,
where terms of a dependently typed lambda calculus to encode safety
proofs.

A special issue of the Journal of Functional Programming will be devoted
to the interplay between dependent type theory and programming practice.
We welcome technical contributions in the field, as well as position
papers that:
 - make researchers in programming languages aware of new developments
   and research directions on the theory side;
 - point out to theorists practical uses of advanced type systems and
   urge them to address theoretical problems arising in emerging
   applications. 

Authors who are concerned about the appropriateness of a topic are welcome
to contact the guest editors. Manuscripts should be unpublished works and
not submitted elsewhere. Revised and enhanced versions of papers published
in conference proceedings that have not appeared in archival journals are
eligible for submission. All submissions will be reviewed according to the
usual standards of scholarship and originality.

Submissions should be sent to Gilles Barthe (Gilles.Barthe@inria.fr), with
a copy to Nasreen Ahmad (nasreen@dcs.gla.ac.uk). Submitted articles should
be sent in postscript format preferably gzipped and uuencoded. In
addition, please send, as plain text, title, abstract, and contact
information.

The submission deadline is December 1st, 2001.

Guest Editors:

   o Gilles Barthe, INRIA Sophia-Antipolis, France
   o Peter Dybjer, Chalmers Tekniska Högskola, Sweden
   o Peter Thiemann, Universität Freiburg, Germany