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:[bull ] make researchers in programming languages aware of new developments and research
directions on the theory side;[bull ] 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 ([email protected]), with a copy to
Nasreen Ahmad ([email protected]). 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.
Proof-term synthesis on dependent-type systems via explicit substitutions
