Call for papers

The Post-Proceedings of the TYPES 2004 Workshop (types2004.lri.fr) will be published, after a formal referee process, as a volume of the Lecture Notes in Computer Science (LNCS) series. Previous TYPES post-workshop proceedings include LNCS volumes 3085, 2646, 2277, 1657, 1512, 1158, 996 and 806.

We encourage you to submit research papers on the subject of the Types Working Group, i.e. the Computer-Assisted Formal Reasoning, an area which is of deep interest for industry. The aim of our research activities is to develop the technology of formal reasoning based on Type Theory by improving the languages and tools of reasoning and by applying the technology in several domains such as programming languages, certified software, and formalisation of mathematics.

Topics include, but are not limited to:

• foundations of type theory and constructive mathematics
• applications of type theory
• programming with type theory
• industrial uses of type theory technology
• meta-theoretic studies of type systems
• implementation of proof-assistants
• automation in computer-assisted reasoning
• links between type theory and functional programming
• formalizing mathematics using type theory

SUBMISSION DEADLINE	April 25, 2005
NOTIFICATION OF ACCEPTANCE	June 30, 2005
FINAL VERSION DUE	August 15, 2005

We hope this volume will give a good account of the papers presented at the workshop and of recent research in the field in general. We invite submission of high quality papers, written in English and typeset in LaTeX2e using the LNCS style. (See authors Instructions at http://www.springeronline.com/lncs). Submissions should not have been published and should not be under consideration for publication elsewhere. Submissions should be no more than fifteen pages long in LNCS style. Please email your contribution as a self-contained pdf file to:

In a separate email, give the title, authors and abstract of your submission, as well as email address of the corresponding author. Submissions will be acknowledged (perhaps with some delay).

LNCS is now published in full-text electronic version, as well as printed books. Thus we will need the final LaTeX source files of accepted submissions. The final versions of accepted submissions must be in the LaTeX2e LNCS style, and be as self-contained as possible. With the final version you will also be asked to fill a copyright form for LNCS accepted papers.

The editors (Jean-Christophe Filliatre, Christine Paulin, and Benjamin Werner).