We encourage you to submit research papers onthe subject of the Types Working Group,i.e. the Computer-Assisted Formal Reasoning, an area which is of deep interestfor industry. The aim of our research activities is to develop the technologyof formal reasoning based on Type Theory by improving the languages and toolsof reasoning and by applying the technology in several domains such as programminglanguages, 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
Also work within the scope of TYPES that was notpresented at the workshop or whose authors are not formally involved in the Working Group can be submitted for the proceedings.
SUBMISSION DEADLINE: Octber 3, 2003.
NOTIFICATION OF ACCEPTANCE: november 30, 2003
FINAL VERSION DUE: january 15
We hope this volume will give a good account of the papers presented atthe workshop and of recent research in the field in general. We invite submissionof high quality papers, written in English and typeset in LaTeX2e using theLNCS style. (See Authors Instructions .)Submissions should not have been published and should not beunder consideration for publication elsewhere. Submissionsshould 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 ofyour submission, as well as email address of thecorresponding author. Submissions will be acknowledged(perhaps with some delay).
LNCS is now published in full-text electronic version, aswell as printed books. Thus we will need the final LaTeXsource files of accepted submissions. The final versions ofaccepted submissions must be in the LaTeX2e LNCS style, andbe as self-contained as possible. With the final version you will also be asked to fill a copyright form for LNCS accepted papers.