The Resource Types for proofs and programs : international workshop, TYPES '99, Lökeberg, Sweden, June 12-16, 1999 : selected papers, Thierry Coquand [and others], (Eds.)

Types for proofs and programs : international workshop, TYPES '99, Lökeberg, Sweden, June 12-16, 1999 : selected papers, Thierry Coquand [and others], (Eds.)

Label
Types for proofs and programs : international workshop, TYPES '99, Lökeberg, Sweden, June 12-16, 1999 : selected papers
Title
Types for proofs and programs
Title remainder
international workshop, TYPES '99, Lökeberg, Sweden, June 12-16, 1999 : selected papers
Statement of responsibility
Thierry Coquand [and others], (Eds.)
Creator
Contributor
Subject
Genre
Language
eng
Member of
Cataloging source
DLC
Illustrations
illustrations
Index
index present
LC call number
QA76.9.A96
LC item number
T96 1999
Literary form
non fiction
http://bibfra.me/vocab/lite/meetingDate
1999
http://bibfra.me/vocab/lite/meetingName
TYPES '99
Nature of contents
bibliography
http://library.link/vocab/relatedWorkOrContributorDate
1961-
http://library.link/vocab/relatedWorkOrContributorName
Coquand, Thierry
http://library.link/vocab/subjectName
  • Automatic theorem proving
  • Computer programming
  • Type theory
  • lambda calcul
  • théorie démonstration
  • système preuve
  • vérification programme
  • théorie type
  • Théorèmes
  • Programmation (Informatique)
  • Types, Théorie des
  • Automatic theorem proving
  • Computer programming
  • Type theory
  • Logica
  • Programmeertalen
  • Kunstmatige intelligentie
  • Théorie des types
  • Théorèmes
  • Ordinateurs
  • Programmierung
  • Reduktionssystem
  • Typentheorie
  • Beweistheorie
  • Formale Methode
  • Rome
  • Lökeberg <1999>
Label
Types for proofs and programs : international workshop, TYPES '99, Lökeberg, Sweden, June 12-16, 1999 : selected papers, Thierry Coquand [and others], (Eds.)
Instantiates
Publication
Bibliography note
Includes bibliographical references and index
Carrier category
volume
Carrier category code
  • nc
Carrier MARC source
rdacarrier
Content category
text
Content type code
  • txt
Content type MARC source
rdacontent
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 <U+00dd>-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
Dimensions
24 cm.
Dimensions
unknown
Extent
193 pages
Isbn
9781579583163
Lccn
00069849
Media category
unmediated
Media MARC source
rdamedia
Media type code
  • n
Specific material designation
remote
System control number
  • (OCoLC)45620936
  • (OCoLC)ocm45620936
Label
Types for proofs and programs : international workshop, TYPES '99, Lökeberg, Sweden, June 12-16, 1999 : selected papers, Thierry Coquand [and others], (Eds.)
Publication
Bibliography note
Includes bibliographical references and index
Carrier category
volume
Carrier category code
  • nc
Carrier MARC source
rdacarrier
Content category
text
Content type code
  • txt
Content type MARC source
rdacontent
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 <U+00dd>-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
Dimensions
24 cm.
Dimensions
unknown
Extent
193 pages
Isbn
9781579583163
Lccn
00069849
Media category
unmediated
Media MARC source
rdamedia
Media type code
  • n
Specific material designation
remote
System control number
  • (OCoLC)45620936
  • (OCoLC)ocm45620936

Library Locations

  • African Studies LibraryBorrow it
    771 Commonwealth Avenue, 6th Floor, Boston, MA, 02215, US
    42.350723 -71.108227
  • Alumni Medical LibraryBorrow it
    72 East Concord Street, Boston, MA, 02118, US
    42.336388 -71.072393
  • Astronomy LibraryBorrow it
    725 Commonwealth Avenue, 6th Floor, Boston, MA, 02445, US
    42.350259 -71.105717
  • Fineman and Pappas Law LibrariesBorrow it
    765 Commonwealth Avenue, Boston, MA, 02215, US
    42.350979 -71.107023
  • Frederick S. Pardee Management LibraryBorrow it
    595 Commonwealth Avenue, Boston, MA, 02215, US
    42.349626 -71.099547
  • Howard Gotlieb Archival Research CenterBorrow it
    771 Commonwealth Avenue, 5th Floor, Boston, MA, 02215, US
    42.350723 -71.108227
  • Mugar Memorial LibraryBorrow it
    771 Commonwealth Avenue, Boston, MA, 02215, US
    42.350723 -71.108227
  • Music LibraryBorrow it
    771 Commonwealth Avenue, 2nd Floor, Boston, MA, 02215, US
    42.350723 -71.108227
  • Pikering Educational Resources LibraryBorrow it
    2 Silber Way, Boston, MA, 02215, US
    42.349804 -71.101425
  • School of Theology LibraryBorrow it
    745 Commonwealth Avenue, 2nd Floor, Boston, MA, 02215, US
    42.350494 -71.107235
  • Science & Engineering LibraryBorrow it
    38 Cummington Mall, Boston, MA, 02215, US
    42.348472 -71.102257
  • Stone Science LibraryBorrow it
    675 Commonwealth Avenue, Boston, MA, 02445, US
    42.350103 -71.103784
Processing Feedback ...