Concrete Semantics : With Isabelle/HOL / / by Tobias Nipkow, Gerwin Klein |
Autore | Nipkow Tobias |
Edizione | [1st ed. 2014.] |
Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 |
Descrizione fisica | 1 online resource (XIII, 298 p. 87 illus., 1 illus. in color.) |
Disciplina | 005.1015113 |
Soggetto topico |
Computer logic
Programming languages (Electronic computers) Mathematical logic Logics and Meanings of Programs Programming Languages, Compilers, Interpreters Mathematical Logic and Formal Languages |
ISBN | 3-319-10542-6 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Introduction -- Programming and Proving -- Case Study: IMP Expressions -- Logic and Proof Beyond Equality -- Isar: A Language for Structured Proofs -- IMP: A Simple Imperative Language -- Compiler -- Types -- Program Analysis -- Denotational Semantics -- Hoare Logic -- Abstract Interpretation -- App. A, Auxiliary Definitions -- App. B, Symbols -- References. |
Record Nr. | UNINA-9910298989403321 |
Nipkow Tobias | ||
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Isabelle/HOL [[electronic resource] ] : A Proof Assistant for Higher-Order Logic / / by Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel |
Autore | Nipkow Tobias |
Edizione | [1st ed. 2002.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 |
Descrizione fisica | 1 online resource (XIV, 226 p.) |
Disciplina | 004.015113 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Mathematical logic
Logic Computers Artificial intelligence Computer logic Programming languages (Electronic computers) Mathematical Logic and Formal Languages Theory of Computation Artificial Intelligence Logics and Meanings of Programs Programming Languages, Compilers, Interpreters |
ISBN | 3-540-45949-9 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Elementary Techniques -- 1. The Basics -- 2. Functional Programming in HOL -- 3. More Functional Programming -- 4. Presenting Theories -- Logic and Sets -- 5. The Rules of the Game -- 6. Sets, Functions, and Relations -- 7. Inductively Defined Sets -- Advanced Material -- 8. More about Types -- 9. Advanced Simplification, Recursion, and Induction -- 10. Case Study: Verifying a Security Protocol. |
Record Nr. | UNISA-996466028903316 |
Nipkow Tobias | ||
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Isabelle/HOL : A Proof Assistant for Higher-Order Logic / / by Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel |
Autore | Nipkow Tobias |
Edizione | [1st ed. 2002.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 |
Descrizione fisica | 1 online resource (XIV, 226 p.) |
Disciplina | 004.015113 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Mathematical logic
Logic Computers Artificial intelligence Computer logic Programming languages (Electronic computers) Mathematical Logic and Formal Languages Theory of Computation Artificial Intelligence Logics and Meanings of Programs Programming Languages, Compilers, Interpreters |
ISBN | 3-540-45949-9 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Elementary Techniques -- 1. The Basics -- 2. Functional Programming in HOL -- 3. More Functional Programming -- 4. Presenting Theories -- Logic and Sets -- 5. The Rules of the Game -- 6. Sets, Functions, and Relations -- 7. Inductively Defined Sets -- Advanced Material -- 8. More about Types -- 9. Advanced Simplification, Recursion, and Induction -- 10. Case Study: Verifying a Security Protocol. |
Record Nr. | UNINA-9910145793603321 |
Nipkow Tobias | ||
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|