A thriving trend in computing science is to seek formal, reliable means of ensuring that programs possess crucial correctness properties.

One path towards this goal is the design of high-level programming languages which enforces that program, by their very own structure, behave correctly. In the past decade, the use of type systems to guarantee that data and program components be used in appropriate ways has enjoyed wide success and is still a main focus both from researchers and developers.

With more expressive type systems, the programmer is allowed to specify more fine-grained properties the program is supposed to hold. Dependent type systems, allowing types to refer to (hence depend on) data, are particularly powerful since they reflect the reality that what defines “appropriate” program behaviours is often dynamic. With the type system, programmers are free to communicate the design of software to computers and negotiate their place in the spectrum of precision from basic memory safety to total correctness.

Dependent types have their origin in the constructive foundations of mathematics, and have played an import role in theorem provers. Advanced proof assistants, such as Coq, has been used to formalise mathematics (e.g. the proof of the four colour theorem) and verify compilers. Only recently have they begun to be integrated into programming languages. The results so far have turned out to be fruitful. A number of dependently typed programming language and systems have been proposed, including Cayenne, DML, Epigram, Ωmega, ATS, Agda, Guru, etc, showing a maturity beyond the proof-of-concept stage. Papers on dependent types submitted to and published in major conferences have significantly increased in number. Some more “mainstream” functional programming languages, such as Haskell, also start to adopt features such as GADT and type family that are strongly influenced by dependent types.

Dependently typed programming, however, is yet to be considered a practical tool and an efficient device to ensure program correctness and to reduce development costs. Many issues remain to be resolved, including but not limited to:

_ design of a small but expressive core language on which to built up a verifiable metatheory;

_ metaprogramming, reflectivity, and the possibility of representing dependently typed terms in a dependently typed language;

_ representing variable-binding and supporting both structural inspection and functional usage;

_ interpreting representations to automate problem solving;

_ separating and redesigning a language of “proof” as distinct from a language for “programming”;

_ integrating extensional reasoning about functions with computation in dependent type systems, while at the same time concealing the internal structure of proofs;

_ modelling interaction and communication in distributed, concurrent systems using dependent types.

This workshop aims to provide a venue for people actively working in this field so that these issues could be discussed.