Types for proofs and programs. International workshop, TYPES 2003, Torino, Italy, April 30 -- May 4, 2003. Revised selected papers. (Q704168)

The articles of this volume will be reviewed individually. The preceding workshop has been reviewed (see Zbl 1019.00007). Indexed articles: \textit{Adams, Robin}, A modular hierarchy of logical frameworks, 1-16 [Zbl 1100.68542] \textit{Alessi, F.; Barbanera, Franco; Dezani-Ciancaglini, Mariangiola}, Tailoring filter models, 17-33 [Zbl 1100.03511] \textit{Ballarin, Clemens}, Locales and locale expressions in Isabelle/Isar, 34-50 [Zbl 1100.68615] \textit{Baro, Sylvain}, Introduction to PAF!, a proof assistant for ML programs verification, 51-65 [Zbl 1100.68543] \textit{Berghofer, Stefan}, A constructive proof of Higman's lemma in Isabelle, 66-82 [Zbl 1100.68616] \textit{Bettini, Lorenzo; Bono, Viviana; Likavec, Silvia}, A core calculus of higher-order mixins and classes, 83-98 [Zbl 1100.68544] \textit{Bono, Viviana; Tiuryn, Jerzy; Urzyczyn, Paweł}, Type inference for nested self types, 99-114 [Zbl 1100.68545] \textit{Brady, Edwin; McBride, Conor; McKinna, James}, Inductive families need not store their indices, 115-129 [Zbl 1100.68546] \textit{Chrząszcz, Jacek}, Modules in Coq are and will be correct, 130-146 [Zbl 1100.68617] \textit{Cirstea, Horatiu; Liquori, Luigi; Wack, Benjamin}, Rewriting calculus with fixpoints: Untyped and first-order systems, 147-161 [Zbl 1100.03514] \textit{Corbineau, Pierre}, First-order reasoning in the calculus of inductive constructions, 162-177 [Zbl 1100.03509] \textit{Dal Lago, Ugo; Martini, Simone; Roversi, Luca}, Higher-order linear ramified recurrence, 178-193 [Zbl 1100.03512] \textit{Espírito Santo, José; Pinto, Luís}, Confluence and strong normalisation of the generalised multiary \(\lambda\)-calculus, 194-209 [Zbl 1100.03513] \textit{Gambino, Nicola; Hyland, Martin}, Wellfounded trees and dependent polynomial functors, 210-225 [Zbl 1100.03055] \textit{Ghilezan, Silvia; Lescanne, Pierre}, Classical proofs, typed processes, and intersection types (ectended abstract), 226-241 [Zbl 1100.03515] \textit{Honsell, Furio; Lenisa, Marina}, ``Wave-style'' geometry of interaction models in Rel are graph-like lambda-models, 242-258 [Zbl 1100.03056] \textit{Kießling, Robert; Luo, Zhaohui}, Coercions in Hindley-Milner systems, 259-275 [Zbl 1100.68534] \textit{Luo, Yong; Luo, Zhaohui}, Combining incoherent coercions for \(\Sigma\)-types, 276-292 [Zbl 1100.03510] \textit{Momigliano, Alberto; Tiu, Alwen}, Induction and co-induction in sequent calculus, 293-308 [Zbl 1100.03516] \textit{Niqui, Milad; Bertot, Yves}, QArith: Coq formalisation of lazy rational arithmetic, 309-323 [Zbl 1100.68619] \textit{Honsell, Furio; Scagnetto, Ivan}, Mobility types in Coq, 324-337 [Zbl 1100.68618] \textit{Soloviev, Sergej; Chemouil, David}, Some algebraic structures in lambda-calculus with inductive types, 338-354 [Zbl 1100.03517] \textit{Watkins, Kevin; Cervesato, Iliano; Pfenning, Frank; Walker, David}, A concurrent logical framework: The propositional fragment, 355-377 [Zbl 1100.68548] \textit{Wiedijk, Freek}, Formal proof sketches, 378-393 [Zbl 1100.68620] \textit{Xi, Hongwei}, Applied type system (extended abstract), 394-408 [Zbl 1100.03518]