Types for proofs and programs : international workshop, TYPES '99, Lökeberg, Sweden, June 12-16, 1999 : selected papers /
| Corporate Author: | |
|---|---|
| Other Authors: | |
| Format: | Conference Proceeding Book |
| Language: | English |
| Published: |
Berlin ; New York :
Springer,
[2000]
|
| Series: | Lecture notes in computer science.
1956. |
| Subjects: |
Table of Contents:
- Specification and verification of a formal system for structurally recursive functions / Andreas Abel
- A predicative strong normalisation proof for a [lambda]-calculus with interleaving inductive types / Andreas Abel and Thorsten Altenkirch
- Polymorphic intersection type assignment for rewrite systems with abstraction and β-rule / Steffen van Bakel, Franco Barbanera, and Maribel Fernández
- Computer-assisted mathematics at work (the Hahn-Banach theorem in Isabelle/Isar) / Gertrud Bauer and Markus Wenzel
- Specification of a smart card operating system / Gustavo Betarte ... [et al.]
- Implementation techniques for inductive types in plastic / Paul Callaghan and Zhaohui Luo
- A co-inductive approach to real numbers / Alberto Ciaffaglione and Pietro Di Gianantonio
- Information retrieval in a Coq proof library using type isomorphisms / David Delahaye
- Memory management : an abstract formulation of incremental tracing / Healfdene Goguen, Richard Brooksby, and Rod Burstall
- The three gap theorem (Steinhaus conjecture) / Micaela Mayero
- Formalising formulas-as-types-as-objects / Qiao Haiyan.