TYPES 1999:
Lökeberg,
Sweden
Thierry Coquand, Peter Dybjer, Bengt Nordström, Jan M. Smith (Eds.):
Types for Proofs and Programs, International Workshop TYPES'99, Lökeberg, Sweden, June 12-16, 1999, Selected Papers.
Lecture Notes in Computer Science 1956 Springer 2000, ISBN 3-540-41517-3 BibTeX
@proceedings{DBLP:conf/types/1999,
editor = {Thierry Coquand and
Peter Dybjer and
Bengt Nordstr{\"o}m and
Jan M. Smith},
title = {Types for Proofs and Programs, International Workshop TYPES'99,
L{\"o}keberg, Sweden, June 12-16, 1999, Selected Papers},
booktitle = {TYPES},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {1956},
year = {2000},
isbn = {3-540-41517-3},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
- Andreas Abel:
Specification and Verification of a Formal System for Structurally Recursive Functions.
1-20
Electronic Edition (Springer LINK) BibTeX
- Andreas Abel, Thorsten Altenkirch:
A Predicative Strong Normalisation Proof for a lambda-Calculus with Interleaving Inductive Types.
21-40
Electronic Edition (Springer LINK) BibTeX
- Steffen van Bakel, Franco Barbanera, Maribel Fernández:
Polymorphic Intersection Type Assignment for Rewrite Systems with Abstractions and beta-Rule.
41-60
Electronic Edition (Springer LINK) BibTeX
- Gertrud Bauer, Markus Wenzel:
Computer-Assisted Mathematics at Work (The Hahn-Banach Theorem in Isabelle/Isar).
61-76
Electronic Edition (Springer LINK) BibTeX
- Gustavo Betarte, Cristina Cornes, Nora Szasz, Alvaro Tasistro:
Specification of a Smart Card Operating System.
77-93
Electronic Edition (Springer LINK) BibTeX
- Paul Callaghan, Zhaohui Luo:
Implementation Techniques for Inductive Types in Plastic.
94-113
Electronic Edition (Springer LINK) BibTeX
- Alberto Ciaffaglione, Pietro Di Gianantonio:
A Co-inductive Approach to Real Numbers.
114-130
Electronic Edition (Springer LINK) BibTeX
- David Delahaye:
Information Retrieval in a Coq Proof Library Using Type Isomorphisms.
131-147
Electronic Edition (Springer LINK) BibTeX
- Healfdene Goguen, Richard Brooksby, Rod M. Burstall:
Memory Management: An Abstract Formulation of Incremental Tracing.
148-161
Electronic Edition (Springer LINK) BibTeX
- Micaela Mayero:
The Three Gap Theorem (Steinhaus Conjecture).
162-173
Electronic Edition (Springer LINK) BibTeX
- Qiao Haiyan:
Formalising Formulas-as-Types-as-Objects.
174-193
Electronic Edition (Springer LINK) BibTeX
Copyright © Sat May 16 23:44:06 2009
by Michael Ley (ley@uni-trier.de)