


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.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














