Accepted Papers: PostProceedings of "TYPES 2003"The PostWorkshop Proceedings forTYPES 2003 will be published as a volume of the Lecture Notes in Computer Science (LNCS) series.Previous TYPES postworkshop proceedings include LNCS volumes 2646, 2277, 1657, 1512, 1158, 996 and 806. The aim of our research activities is to develop the technology of 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
 metatheoretic studies of type systems
 implementation of proofassistants
 automation in computerassisted reasoning
 links between type theory and functional programming
 formalizing mathematics using type theory
LIST OF ACCEPTED PAPERS: A. Momigliano, A. Tiu Induction and Coinduction in Sequent Calculus C. Ballarin Locales and Locale Expressions in Isabelle/Isar E. Brady, C. McBride, J. McKinna Inductive Families Need Not Store Their Indices F. Alessi, F. Barbanera, M. DezaniCiancaglini Tailoring Filter Models F. Honsell, M. Lenisa “Wavestyle” Geometry of Interaction Models in Rel are Graphlike Lambdamodels F. Wiedijk Formal proof sketches H. Cirstea, L. Liquori, B. Wack Rewriting Calculus with Fixpoints: Untyped and Firstorder Systems Hongwei Xi Applied Type System I. Scagnetto, F. Honsell Mobility types in Coq J. Chrzˇszcz Modules in Coq Are and Will Be Correct J. Espirito Santo, L. Pinto Confluence and Strong Normalisation of the Generalised Multiary lambdacalculus K. Watkins, I. Cervesato, F. Pfenning, D. Walker A Concurrent Logical Framework: The Propositional Fragment L. Bettini, V. Bono, S. Likavec A Core Calculus of HigherOrder Mixins and Classes M. Niqui, Y. Bertot QArith: Coq Formalisation of Lazy Rational Arithmetic N. Gambino, M. Hyland Wellfounded Trees and Dependent Polynomial Functors P. Corbineau First order reasoning in the Calculus of Inductive Constructions R. Adams A Modular Hierarchy of Logical Frameworks R. Kiebling, Zhaohui Luo Coercions in HindleyMilner systems S. Baro Introduction to PAF!, a Proof Assistant for ML Programs Veri cation S. Berghofer A constructive proof of Higman's lemma in Isabelle S. Gilezan, P. Lescanne Classical proofs, typed processes and intersection types S. Soloviev, D. Chemouil Some algebraic structures …. U. DelLago, S. Martini, L. Roversi Higher order linear ramified recurrence V. Bono, J. Tiuryn, P. Urzyczyn Type inference for nested self types Yong Luo, Zhaohui Luo Combinig incoherent coercions for Sigmatypes 
FINAL VERSION DUE: January, 30
Papers should be written in English and typeset in LaTeX2e using theLNCS style. (See Authors Instructions ). Final papers should be no more than fifteen pages long in LNCS style. LNCS is now published in fulltext electronic version, aswell as printed books. The final versions of accepted submissions must be in the LaTeX2e LNCS style, andbe as selfcontained as possible. With the final version you will also be asked to fill a copyright form for LNCS accepted papers. Best regards from the editors, Stefano Berardi, Mario Coppo, Ferruccio Damiani . Send your questions and comments totypes2003@di.unito.it
