Abstract is missing.
- Specification and Verification of a Formal System for Structurally Recursive FunctionsAndreas Abel. 1-20 [doi]
- A Predicative Strong Normalisation Proof for a lambda-Calculus with Interleaving Inductive TypesAndreas Abel, Thorsten Altenkirch. 21-40 [doi]
- Polymorphic Intersection Type Assignment for Rewrite Systems with Abstractions and ::::beta::::-RuleSteffen van Bakel, Franco Barbanera, Maribel Fernández. 41-60 [doi]
- Computer-Assisted Mathematics at Work (The Hahn-Banach Theorem in Isabelle/Isar)Gertrud Bauer, Markus Wenzel. 61-76 [doi]
- Specification of a Smart Card Operating SystemGustavo Betarte, Cristina Cornes, Nora Szasz, Alvaro Tasistro. 77-93 [doi]
- Implementation Techniques for Inductive Types in PlasticPaul Callaghan, Zhaohui Luo. 94-113 [doi]
- A Co-inductive Approach to Real NumbersAlberto Ciaffaglione, Pietro Di Gianantonio. 114-130 [doi]
- Information Retrieval in a Coq Proof Library Using Type IsomorphismsDavid Delahaye. 131-147 [doi]
- Memory Management: An Abstract Formulation of Incremental TracingHealfdene Goguen, Richard Brooksby, Rod M. Burstall. 148-161 [doi]
- The Three Gap Theorem (Steinhaus Conjecture)Micaela Mayero. 162-173 [doi]
- Formalising Formulas-as-Types-as-ObjectsQiao Haiyan. 174-193 [doi]