Vai al contenuto principale della pagina
Titolo: |
Types 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 Pollack
![]() |
Pubblicazione: | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 |
Edizione: | 1st ed. 2002. |
Descrizione fisica: | 1 online resource (VIII, 248 p.) |
Disciplina: | 006.3/33 |
Soggetto topico: | Computer 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 | |
Persona (resp. second.): | CallaghanPaul |
LuoZhaohui | |
McKinnaJames | |
PollackRobert | |
Note generali: | Bibliographic Level Mode of Issuance: Monograph |
Nota di bibliografia: | Includes bibliographical references at the end of each chapters and index. |
Nota di contenuto: | 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. |
Titolo autorizzato: | Types for Proofs and Programs ![]() |
ISBN: | 3-540-45842-5 |
Formato: | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione: | Inglese |
Record Nr.: | 996465407003316 |
Lo trovi qui: | Univ. di Salerno |
Opac: | Controlla la disponibilità qui |