Types for proofs and programs. International workshop, TYPES '98. Kloster Irsee, Germany, March 27--31, 1999. Selected papers (Q1819249)

The articles of this volume will be reviewed individually. Indexed articles: \textit{Aczel, Peter}, On relating type theories and set theories, 1-18 [Zbl 0944.03056] \textit{Ahn, René; Borghuis, Tijn}, Communication modelling and context-dependent interpretation: An integrated approach, 19-32 [Zbl 0938.68843] \textit{Coquand, Thierry; Persson, Henrik}, Gröbner bases in type theory, 33-46 [Zbl 0979.03044] \textit{Despeyroux, Joëlle; Leleu, Pierre}, A modal lambda calculus with iteration and case constructs, 47-61 [Zbl 0943.03010] \textit{Dowek, Gilles; Werner, Benjamin}, Proof normalization modulo, 62-77 [Zbl 0944.03052] \textit{Filliâtre, Jean-Christophe}, Proof of imperative programs in type theory, 78-92 [Zbl 0944.03021] \textit{Fridlender, Daniel}, An interpretation of the fan theorem in type theory, 93-105 [Zbl 0943.03047] \textit{Goubault-Larrecq, Jean}, Conjunctive types and SKInT, 106-120 [Zbl 0943.03011] \textit{Kammüller, Florian}, Modular structures as dependent types in Isabelle, 121-132 [Zbl 0942.68116] \textit{Kleymann, Thomas}, Metatheory of verification calculi in LEGO. To what extent does syntax matter?, 133-148 [Zbl 0942.68117] \textit{Liquori, Luigi}, Bounded polymorphism for extensible objects, 149-163 [Zbl 0942.68028] \textit{Maietti, Maria Emilia}, About effective quotients in constructive type theory, 164-178 [Zbl 0943.03053] \textit{Pfenning, Frank; Schürmann, Carsten}, Algorithms for equality and unification in the presence of notational definitions, 179-193 [Zbl 0942.03014] \textit{Sambin, Giovanni; Gebellato, Silvia}, A preview of the basic picture: A new perspective on formal topology, 194-207 [Zbl 0953.03069]