Types for proofs and programs. 3rd international workshop, TYPES '99, Lökeberg, Sweden, June 12--16, 1999. Selected papers
type: Item
instance of: scholarly article
title: Types for proofs and programs. 3rd international workshop, TYPES '99, Lökeberg, Sweden, June 12--16, 1999. Selected papers
zbMATH Open document ID: 0953.00042
published in: Lecture Notes in Computer Science
publication date: 2001-01-10T00:00:00Z
review text: 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]
Mathematics Subject Classification ID: 00B25
Mathematics Subject Classification ID: 68-06
Mathematics Subject Classification ID: 03-06
zbMATH DE Number: 1550309
zbMATH Keywords: Lökeberg (Sweden)
zbMATH Keywords: Selected papers
zbMATH Keywords: Workshop
zbMATH Keywords: TYPES '99
zbMATH Keywords: Types for proofs
zbMATH Keywords: Types for programs
describes a project that uses: Coq
MaRDI profile type: Publication
Recommended article: Types for proofs and programs. International Workshop TYPES '94, Båstad, Sweden, June 6-10, 1994. Selected papers
Recommended article: Types for proofs and programs. International workshop, TYPES '98. Kloster Irsee, Germany, March 27--31, 1999. Selected papers
Recommended article: TYPES '93, Types for proofs and programs. International Workshop, Nijmegen, the Netherlands, May 24-28, 1993. Selected papers
Recommended article: Types for proofs and programs. International workshop TYPES '95, Torino, Italy, June 5--8, 1995. Selected papers
Recommended article: Types for proofs and programs. International workshop TYPES '96, Aussois, France, December 15--19, 1996. Selected papers
Recommended article: Types for proofs and programs. International workshop, TYPES 2003, Torino, Italy, April 30 -- May 4, 2003. Revised selected papers.
Recommended article: Types for proofs and programs. International workshop, TYPES 2000, Durham, GB, December 8--12, 2000. Selected papers
Recommended article: Types for proofs and programs. International workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24--28, 2002. Selected papers
Recommended article: Types for proofs and programs. International workshop, TYPES 2006, Nottingham, UK, April 18--21, 2006. Revised selected papers.
Recommended article: Q3174684
description: scientific article; zbMATH DE number 1550309