Dependent Type Theory Meets Programming Practice
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:
Submissions should be sent to Gilles Barthe (Gilles.Barthe@inria.fr), with a copy to Nasreen Ahmad (firstname.lastname@example.org). 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.