Types for proofs and programs. International workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24--28, 2002. Selected papers (Q1408067)

The articles of this volume will be reviewed individually. The preceding workshop has been reviewed (see Zbl 0988.00060). Indexed articles: \textit{Abel, Andreas; Matthes, Ralph}, (Co-)Iteration for higher-order nested datatypes, 1-20 [Zbl 1023.68066] \textit{Berghofer, Stefan}, Program extraction in simply-typed higher order logic, 21-38 [Zbl 1023.68021] \textit{Bove, Ana}, General recursion in type theory, 39-58 [Zbl 1023.03532] \textit{Brucker, Achim D.; Wolff, Burkhart}, Using theory morphisms for implementing formal methods tools, 59-77 [Zbl 1023.68654] \textit{Carlström, Jesper}, Subsets, quotients and partial functions in Martin-Löf's type theory, 78-94 [Zbl 1023.03021] \textit{Chicli, Laurent; Pottier, Loïc; Simpson, Carlos}, Mathematical quotients and quotient types in Coq, 95-107 [Zbl 1023.03534] \textit{Cruz-Filipe, Luís}, A constructive formalization of the fundamental theorem of calculus, 108-126 [Zbl 1023.03059] \textit{Dezani-Ciancaglini, Mariangiola; Ghilezan, Silvia}, Two behavioural lambda models, 127-147 [Zbl 1023.03022] \textit{Di Gianantonio, Pietro; Miculan, Marino}, A unifying approach to recursive and co-recursive definitions, 148-161 [Zbl 1023.68022] \textit{Jojgov, Georgi I.}, Holes with binding power, 162-181 [Zbl 1023.68087] \textit{Konečný, Michal}, Typing with conditions and guarantees for functional in-place update, 182-199 [Zbl 1023.68016] \textit{Letouzey, Pierre}, A new extraction for Coq, 200-219 [Zbl 1023.68516] \textit{Luo, Yong; Luo, Zhaohui; Soloviev, Sergei}, Weak transitivity in coercive subtyping, 220-239 [Zbl 1023.68017] \textit{Miquel, Alexandre; Werner, Benjamin}, The not so simple proof-irrelevant model of CC, 240-258 [Zbl 1023.03024] \textit{Nipkow, Tobias}, Structured proofs in Isar/HOL, 259-278 [Zbl 1023.68657] \textit{Setzer, Anton}, Java as a functional programming language, 279-298 [Zbl 1023.68018] \textit{Uustalu, Tarmo}, Monad translating inductive and coinductive types, 299-315 [Zbl 1023.68019] \textit{Vaillant, Stéphane}, A finite first-order presentation of set theory, 316-330 [Zbl 1023.03047]