Accepted Papers: Post-Proceedings of "TYPES 2003"The Post-Workshop Proceedings forTYPES 2003 will be published as a volume of the Lecture Notes in Computer Science (LNCS) series.Previous TYPES post-workshop 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
- 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
LIST OF ACCEPTED PAPERS: A. Momigliano, A. Tiu Induction and Co-induction 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. Dezani-Ciancaglini Tailoring Filter Models F. Honsell, M. Lenisa “Wave-style” Geometry of Interaction Models in Rel are Graph-like Lambda-models F. Wiedijk Formal proof sketches H. Cirstea, L. Liquori, B. Wack Rewriting Calculus with Fixpoints: Untyped and First-order 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 lambda-calculus 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 Higher-Order 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 Hindley-Milner 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 Sigma-types
|
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 full-text electronic version, aswell as printed books. The final versions of accepted 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. Best regards from the editors, Stefano Berardi, Mario Coppo, Ferruccio Damiani .
Send your questions and comments totypes2003@di.unito.it
|
