default search action
TYPES 1999: Lökeberg, Sweden
- Thierry Coquand, Peter Dybjer, Bengt Nordström, Jan M. Smith:
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
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.