Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
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
| 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 |
| Edizione | [1st ed. 2002.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 |
| Descrizione fisica | 1 online resource (VIII, 248 p.) |
| Disciplina | 006.3/33 |
| Collana | Lecture Notes in Computer Science |
| 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 |
| ISBN | 3-540-45842-5 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| 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. |
| Record Nr. | UNISA-996465407003316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Types for Proofs and Programs : International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000. Selected Papers / / edited by Paul Callaghan, Zhaohui Luo, James McKinna, Robert Pollack
| Types for Proofs and Programs : International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000. Selected Papers / / edited by Paul Callaghan, Zhaohui Luo, James McKinna, Robert Pollack |
| Edizione | [1st ed. 2002.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 |
| Descrizione fisica | 1 online resource (VIII, 248 p.) |
| Disciplina | 006.3/33 |
| Collana | Lecture Notes in Computer Science |
| 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 |
| ISBN | 3-540-45842-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| 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. |
| Record Nr. | UNINA-9910143915203321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||