The Resource Types for proofs and programs : International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000 : selected papers, Paul Callaghan [and others]

Types for proofs and programs : International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000 : selected papers, Paul Callaghan [and others]

Label
Types for proofs and programs : International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000 : selected papers
Title
Types for proofs and programs
Title remainder
International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000 : selected papers
Statement of responsibility
Paul Callaghan [and others]
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 2000
Literary form
non fiction
http://bibfra.me/vocab/lite/meetingDate
2000
http://bibfra.me/vocab/lite/meetingName
TYPES 2000
Nature of contents
bibliography
http://library.link/vocab/relatedWorkOrContributorDate
1970-
http://library.link/vocab/relatedWorkOrContributorName
Callaghan, Paul
http://library.link/vocab/subjectName
  • Automatic theorem proving
  • Computer programming
  • programmation en logique
  • sémantique programme
  • théorie programmation
  • réécriture
  • lambda calcul
  • méthode formelle
  • système preuve
  • preuve programme
  • théorie type
  • Théorèmes
  • Programmation (Informatique)
  • Automatic theorem proving
  • Computer programming
  • Logica
  • Programmeertalen
  • Kunstmatige intelligentie
  • Théorèmes
  • Ordinateurs
  • Beweistheorie
  • Kongress
  • Programmierung
  • Reduktionssystem
  • Typentheorie
  • Typsystem
Label
Types for proofs and programs : International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000 : selected papers, Paul Callaghan [and others]
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
Collection Principles in Dependent Type Theory / Peter Aczel and Nicola Gambino -- Executing Higher Order Logic / Stefan Berghofer and Tobias Nipkow -- A Tour with Constructive Real Numbers / Alberto Ciaffaglione and Pietro Di Gianantonio -- An Implementation of Type:Type / Thierry Coquand and Makoto Takeyama -- On the Logical Content of Computational Type Theory: A Solution to Curry's Problem / Matt Fairtlough and Michael Mendler -- Constructive Reals in Coq: Axioms and Categoricity / Herman Geuvers and Milad Niqui -- A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals / Herman Geuvers, Freck Wiedijk and Jan Zwanenburg -- A Kripke-Style Model for the Admissibility of Structural Rules / Healfdene Goguen -- Towards Limit Computable Mathematics / Susumu Hayashi and Masahiro Nakata -- Formalizing the Halting Problem in a Constructive Type Theory / Kristofer Johannisson -- On the Proofs of Some Formally Unprovable Propositions and Prototype Proofs in Type Theory / Giuseppe Longo -- Changing Data Structures in Type Theory: A Study of Natural Numbers / Nicolas Magaud and Yves Bertot -- Elimination with a Motive / Conor McBride -- Generalization in Type Theory Based Proof Assistants / Olivier Pons -- An Inductive Version of Nash-Williams' Minimal-Bad-Sequence Argument for Higman's Lemma / Monika Seisenberger
Dimensions
24 cm.
Dimensions
unknown
Extent
viii, 242 pages
Isbn
9783540432876
Lccn
2002022188
Media category
unmediated
Media MARC source
rdamedia
Media type code
  • n
Other physical details
illustrations
Specific material designation
remote
System control number
  • (OCoLC)49197579
  • (OCoLC)ocm49197579
Label
Types for proofs and programs : International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000 : selected papers, Paul Callaghan [and others]
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
Collection Principles in Dependent Type Theory / Peter Aczel and Nicola Gambino -- Executing Higher Order Logic / Stefan Berghofer and Tobias Nipkow -- A Tour with Constructive Real Numbers / Alberto Ciaffaglione and Pietro Di Gianantonio -- An Implementation of Type:Type / Thierry Coquand and Makoto Takeyama -- On the Logical Content of Computational Type Theory: A Solution to Curry's Problem / Matt Fairtlough and Michael Mendler -- Constructive Reals in Coq: Axioms and Categoricity / Herman Geuvers and Milad Niqui -- A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals / Herman Geuvers, Freck Wiedijk and Jan Zwanenburg -- A Kripke-Style Model for the Admissibility of Structural Rules / Healfdene Goguen -- Towards Limit Computable Mathematics / Susumu Hayashi and Masahiro Nakata -- Formalizing the Halting Problem in a Constructive Type Theory / Kristofer Johannisson -- On the Proofs of Some Formally Unprovable Propositions and Prototype Proofs in Type Theory / Giuseppe Longo -- Changing Data Structures in Type Theory: A Study of Natural Numbers / Nicolas Magaud and Yves Bertot -- Elimination with a Motive / Conor McBride -- Generalization in Type Theory Based Proof Assistants / Olivier Pons -- An Inductive Version of Nash-Williams' Minimal-Bad-Sequence Argument for Higman's Lemma / Monika Seisenberger
Dimensions
24 cm.
Dimensions
unknown
Extent
viii, 242 pages
Isbn
9783540432876
Lccn
2002022188
Media category
unmediated
Media MARC source
rdamedia
Media type code
  • n
Other physical details
illustrations
Specific material designation
remote
System control number
  • (OCoLC)49197579
  • (OCoLC)ocm49197579

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 ...