Data Portal @ linkeddatafragments.org

Matches in Harvard for { <http://id.lib.harvard.edu/aleph/008656082/catalog> ?p ?o. }

• catalog abstract "This book contains a selection of papers presented at the third annual workshop of the Esprit Working Group 21900 Types, which was held 12 - 16 June 1999 at L¨okeberg in the rural area north of G¨oteborg and close to Marstrand. It was attended by 77 researchers. The two previous workshops of the working group were held in Aussois, France, in December 1996 and in Irsee, Germany, in March 1998. The proc- dings of those workshops appear as LNCS Vol. 1512 (edited by Christine Paulin- Mohring and Eduardo Gimenez) and LNCS Vol. 1657 (edited by Thorsten - tenkirch, Wolfgang Naraschewski, and Bernhard Reus). These workshops are, in turn, a continuation of the meetings organized in 1993, 1994, and 1995 under the auspices of the Esprit Basic Research Action 6453 Types for Proofs and Programs. Those proceedings were also published in the LNCS series, edited by Henk Barendregt and Tobias Nipkow (Vol. 806, 1993), by Peter Dybjer, Bengt Nordstr¨om, and Jan Smith (Vol. 996, 1994) and by Stefano Berardi and Mario Coppo (Vol. 1158, 1995). The Esprit BRA 6453 was a continuation of the former Esprit Action 3245 Logical Frameworks: - sign, Implementation and Experiments. The articles from the annual workshops organized under that Action were edited by Gerard Huet and Gordon Plotkin in the books Logical Frameworks and Logical Environments, both published by Cambridge University Press.".
• catalog contributor b12125095.
• catalog contributor b12125096.
• catalog created "2001.".
• catalog date "2001".
• catalog date "2001.".
• catalog dateCopyrighted "2001.".
• catalog description "Includes bibliographical references and index.".
• catalog description "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 [beta]-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 [and others] -- 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.".
• catalog description "This book contains a selection of papers presented at the third annual workshop of the Esprit Working Group 21900 Types, which was held 12 - 16 June 1999 at L¨okeberg in the rural area north of G¨oteborg and close to Marstrand. It was attended by 77 researchers. The two previous workshops of the working group were held in Aussois, France, in December 1996 and in Irsee, Germany, in March 1998. The proc- dings of those workshops appear as LNCS Vol. 1512 (edited by Christine Paulin- Mohring and Eduardo Gimenez) and LNCS Vol. 1657 (edited by Thorsten - tenkirch, Wolfgang Naraschewski, and Bernhard Reus). These workshops are, in turn, a continuation of the meetings organized in 1993, 1994, and 1995 under the auspices of the Esprit Basic Research Action 6453 Types for Proofs and Programs. Those proceedings were also published in the LNCS series, edited by Henk Barendregt and Tobias Nipkow (Vol. 806, 1993), by Peter Dybjer, Bengt Nordstr¨om, and Jan Smith (Vol. 996, 1994) and by Stefano Berardi and Mario Coppo (Vol. 1158, 1995). The Esprit BRA 6453 was a continuation of the former Esprit Action 3245 Logical Frameworks: - sign, Implementation and Experiments. The articles from the annual workshops organized under that Action were edited by Gerard Huet and Gordon Plotkin in the books Logical Frameworks and Logical Environments, both published by Cambridge University Press.".
• catalog extent "193 p. :".
• catalog identifier "3540415173 (softcover : alk. paper)".
• catalog isPartOf "Lecture notes in computer science ; 1956".
• catalog issued "2001".
• catalog issued "2001.".
• catalog language "eng".
• catalog publisher "Berlin ; New York : Springer,".
• catalog subject "005.13/1 21".
• catalog subject "Artificial intelligence.".
• catalog subject "Automatic theorem proving Congresses.".
• catalog subject "Computer programming Congresses.".
• catalog subject "Computer science.".
• catalog subject "Logic design.".
• catalog subject "Logic, Symbolic and mathematical.".
• catalog subject "QA76.9.A96 T96 1999".
• catalog subject "Type theory Congresses.".
• catalog tableOfContents "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 [beta]-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 [and others] -- 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.".
• catalog title "Types for proofs and programs : international workshop, TYPES '99, Lökeberg, Sweden, June 12-16, 1999 : selected papers / Thierry Coquand ... [et al.], (Eds.)".
• catalog type "Conference proceedings. fast".
• catalog type "text".