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 
- Andreas Abel:
Specification and Verification of a Formal System for Structurally Recursive Functions.
1-20
- Andreas Abel, Thorsten Altenkirch:
A Predicative Strong Normalisation Proof for a lambda-Calculus with Interleaving Inductive Types.
21-40
- Steffen van Bakel, Franco Barbanera, Maribel Fernández:
Polymorphic Intersection Type Assignment for Rewrite Systems with Abstractions and beta-Rule.
41-60
- Gertrud Bauer, Markus Wenzel:
Computer-Assisted Mathematics at Work (The Hahn-Banach Theorem in Isabelle/Isar).
61-76
- Gustavo Betarte, Cristina Cornes, Nora Szasz, Alvaro Tasistro:
Specification of a Smart Card Operating System.
77-93
- Paul Callaghan, Zhaohui Luo:
Implementation Techniques for Inductive Types in Plastic.
94-113
- Alberto Ciaffaglione, Pietro Di Gianantonio:
A Co-inductive Approach to Real Numbers.
114-130
- David Delahaye:
Information Retrieval in a Coq Proof Library Using Type Isomorphisms.
131-147
- Healfdene Goguen, Richard Brooksby, Rod M. Burstall:
Memory Management: An Abstract Formulation of Incremental Tracing.
148-161
- Micaela Mayero:
The Three Gap Theorem (Steinhaus Conjecture).
162-173
- Qiao Haiyan:
Formalising Formulas-as-Types-as-Objects.
174-193
Last update Thu May 23 08:37:47 2013
CET by the DBLP Team — 
Data released under the ODC-BY 1.0 license — See also our legal information page
