04331nam 22007695 450 99646540700331620200702125154.03-540-45842-510.1007/3-540-45842-5(CKB)1000000000211678(SSID)ssj0000327459(PQKBManifestationID)11265772(PQKBTitleCode)TC0000327459(PQKBWorkID)10301621(PQKB)10491463(DE-He213)978-3-540-45842-5(MiAaPQ)EBC3072895(PPN)155232916(EXLCZ)99100000000021167820121227d2002 u| 0engurnn|008mamaatxtccrTypes for Proofs and Programs[electronic resource] International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000. Selected Papers /edited by Paul Callaghan, Zhaohui Luo, James McKinna, Robert Pollack1st ed. 2002.Berlin, Heidelberg :Springer Berlin Heidelberg :Imprint: Springer,2002.1 online resource (VIII, 248 p.) Lecture Notes in Computer Science,0302-9743 ;2277Bibliographic Level Mode of Issuance: Monograph3-540-43287-6 Includes bibliographical references at the end of each chapters and index.Collection Principles in Dependent Type Theory -- Executing Higher Order Logic -- A Tour with Constructive Real Numbers -- An Implementation of Type:Type -- On the Logical Content of Computational Type Theory: A Solution to Curry’s Problem -- Constructive Reals in Coq: Axioms and Categoricity -- A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals -- A Kripke-Style Model for the Admissibility of Structural Rules -- Towards Limit Computable Mathematics -- Formalizing the Halting Problem in a Constructive Type Theory -- On the Proofs of Some Formally Unprovable Propositions and Prototype Proofs in Type Theory -- Changing Data Structures in Type Theory: A Study of Natural Numbers -- Elimination with a Motive -- Generalization in Type Theory Based Proof Assistants -- An Inductive Version of Nash-Williams’ Minimal-Bad-Sequence Argument for Higman’s Lemma.Lecture Notes in Computer Science,0302-9743 ;2277Computer logicArchitecture, ComputerMathematical logicProgramming languages (Electronic computers)Artificial intelligenceLogics and Meanings of Programshttps://scigraph.springernature.com/ontologies/product-market-codes/I1603XComputer System Implementationhttps://scigraph.springernature.com/ontologies/product-market-codes/I13057Mathematical Logic and Foundationshttps://scigraph.springernature.com/ontologies/product-market-codes/M24005Mathematical Logic and Formal Languageshttps://scigraph.springernature.com/ontologies/product-market-codes/I16048Programming Languages, Compilers, Interpretershttps://scigraph.springernature.com/ontologies/product-market-codes/I14037Artificial Intelligencehttps://scigraph.springernature.com/ontologies/product-market-codes/I21000Computer logic.Architecture, Computer.Mathematical logic.Programming languages (Electronic computers).Artificial intelligence.Logics and Meanings of Programs.Computer System Implementation.Mathematical Logic and Foundations.Mathematical Logic and Formal Languages.Programming Languages, Compilers, Interpreters.Artificial Intelligence.006.3/33Callaghan Pauledthttp://id.loc.gov/vocabulary/relators/edtLuo Zhaohuiedthttp://id.loc.gov/vocabulary/relators/edtMcKinna Jamesedthttp://id.loc.gov/vocabulary/relators/edtPollack Robertedthttp://id.loc.gov/vocabulary/relators/edtTYPES 2000BOOK996465407003316Types for Proofs and Programs771867UNISA