Dependently typed programming is using the power of dependent types to capture relationships between data, internalising invariants necessary for appropriate computation. When data describe types, we can express patterns of programming in code. To capture this potential a number of languages have been proposed and implemented which incorporate some aspects of dependent types, e.g. Agda, ATS, Cayenne, Coq's CIC, Concoqtion, DML, Delphin, ELF, Epigram, Omega, OpTT, Pie, PiSigma, Ynot for a non-exhaustive list.
Within the European TYPES project we have organized two workshops to discuss aspects of dependently typed programming:
The special issue is motivated by the desire to give people who have presented their ideas at those workshops the opportunity to publish papers on their work. However, we would like to invite everybody working in this area to submit papers to the special issue. For a more complete list of topics, please consult the workshop pages following the links above.
The paper should follow the usual standards of journal papers, and should be submitted by email (preferable pdf) to one of the editors before 1 October 2008. We expect that the papers don't exceed 20 pages (see the FI webpage for style files). We hope to be able to stick to the following schedule: