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.
Intelligent Computer Mathematics [[electronic resource] ] : 11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012, Bremen, Germany, July 8-13, 2012, Proceedings / / edited by Johan Jeuring, John Campbell, Jacques Carette, Gabriel Dos Reis, Petr Sojka, Makarius Wenzel, Volker Sorge
| Intelligent Computer Mathematics [[electronic resource] ] : 11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012, Bremen, Germany, July 8-13, 2012, Proceedings / / edited by Johan Jeuring, John Campbell, Jacques Carette, Gabriel Dos Reis, Petr Sojka, Makarius Wenzel, Volker Sorge |
| Edizione | [1st ed. 2012.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2012 |
| Descrizione fisica | 1 online resource (XVIII, 473 p. 117 illus.) |
| Disciplina | 005.131 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Computer science—Mathematics
Artificial intelligence Mathematical logic Computer logic Information storage and retrieval Symbolic and Algebraic Manipulation Artificial Intelligence Math Applications in Computer Science Mathematical Logic and Formal Languages Logics and Meanings of Programs Information Storage and Retrieval |
| ISBN | 3-642-31374-4 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISA-996465534503316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2012 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Theorem Proving in Higher Order Logics [[electronic resource] ] : 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009, Proceedings / / edited by Stefan Berghofer, Tobias Nipkow, Christian Urban, Makarius Wenzel
| Theorem Proving in Higher Order Logics [[electronic resource] ] : 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009, Proceedings / / edited by Stefan Berghofer, Tobias Nipkow, Christian Urban, Makarius Wenzel |
| Edizione | [1st ed. 2009.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 |
| Descrizione fisica | 1 online resource (XI, 517 p.) |
| Disciplina | 004.0151 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Machine theory Computer science—Mathematics Discrete mathematics Algorithms Theory of Computation Formal Languages and Automata Theory Computer Science Logic and Foundations of Programming Mathematics of Computing Discrete Mathematics in Computer Science |
| ISBN | 3-642-03359-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Papers -- Let’s Get Physical: Models and Methods for Real-World Security Protocols -- VCC: A Practical System for Verifying Concurrent C -- Without Loss of Generality -- Invited Tutorials -- HOL Light: An Overview -- A Brief Overview of Mizar -- A Brief Overview of Agda – A Functional Language with Dependent Types -- The Twelf Proof Assistant -- Regular Papers -- Hints in Unification -- Psi-calculi in Isabelle -- Some Domain Theory and Denotational Semantics in Coq -- Turning Inductive into Equational Specifications -- Formalizing the Logic-Automaton Connection -- Extended First-Order Logic -- Formalising Observer Theory for Environment-Sensitive Bisimulation -- Formal Certification of a Resource-Aware Language Implementation -- A Certified Data Race Analysis for a Java-like Language -- Formal Analysis of Optical Waveguides in HOL -- The HOL-Omega Logic -- A Purely Definitional Universal Domain -- Types, Maps and Separation Logic -- Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence -- Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL -- Packaging Mathematical Structures -- Practical Tactics for Separation Logic -- Verified LISP Implementations on ARM, x86 and PowerPC -- Trace-Based Coinductive Operational Semantics for While -- A Better x86 Memory Model: x86-TSO -- Formal Verification of Exact Computations Using Newton’s Method -- Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL -- A Hoare Logic for the State Monad -- Certification of Termination Proofs Using CeTA -- A Formalisation of Smallfoot in HOL -- Liveness Reasoning with Isabelle/HOL -- Mind the Gap. |
| Record Nr. | UNISA-996465644003316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||