Types for proofs and programs. 3rd international workshop, TYPES '99, Lökeberg, Sweden, June 12--16, 1999. Selected papers (Q1591869)

The articles of this volume will be reviewed individually. The preceding workshop (2nd, 1998) has been reviewed (see Zbl 0929.00065). Indexed articles: \textit{Abel, Andreas}, Specification and verification of a formal system for structurally recursive functions, 1-20 [Zbl 0988.68054] \textit{Abel, Andreas; Altenkirch, Thorsten}, A predicative strong normalisation proof for a \(\lambda\)-calculus with interleaving inductive types, 21-40 [Zbl 0988.03029] \textit{van Bakel, Steffen; Barbanera, Franco; Fernández, Maribel}, Polymorphic intersection type assignment for rewrite systems with abstraction and \(\beta\)-rule, 41-60 [Zbl 0988.68092] \textit{Bauer, Gertrud; Wenzel, Markus}, Computer-assisted mathematics at work. The Hahn-Banach theorem in Isabelle/Isar, 61-76 [Zbl 0988.68166] \textit{Betarte, Gustavo; Cornes, Cristina; Szasz, Nora; Tasistro, Alvaro}, Specification of a smart card operating system, 77-93 [Zbl 0988.68741] \textit{Callaghan, Paul; Luo, Zhaohui}, Implementation techniques for inductive types in Plastic, 94-113 [Zbl 0988.68053] \textit{Ciaffaglione, Alberto; Di Gianantonio, Pietro}, A co-inductive approach to real numbers, 114-130 [Zbl 0988.68161] \textit{Delahaye, David}, Information retrieval in a Coq proof library using type isomorphisms, 131-147 [Zbl 0988.68542] \textit{Goguen, Healfdene; Brooksby, Richard; Burstall, Rod}, Memory management: An abstract formulation of incremental tracing, 148-161 [Zbl 0988.68500] \textit{Mayero, Micaela}, The three gap theorem (Steinhaus conjecture), 162-173 [Zbl 0990.11045] \textit{Qiao, Haiyan}, Formalising formulas-as-types-as-objects, 174-193 [Zbl 0988.03028]