| |
|
|
|
|
|
|
|
|
1. |
Record Nr. |
UNISA996396660903316 |
|
|
Autore |
Burnet Gilbert <1643-1715.> |
|
|
Titolo |
An essay on the memory of the late Queen [[electronic resource] /] / by Gilbert, Bishop of Sarum |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
London, : Printed for Ric. Chiswell ..., 1696 |
|
|
|
|
|
|
|
Edizione |
[The second edition.] |
|
|
|
|
|
Descrizione fisica |
|
[2], 5-197, [3] p., 1 leaf of plates : port |
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
Advertisement: p. 197-[3] at end. |
Reproduction of original in Huntington Library. |
|
|
|
|
|
|
|
|
Sommario/riassunto |
|
|
|
|
|
|
|
|
|
|
|
|
|
2. |
Record Nr. |
UNISA996465287103316 |
|
|
Titolo |
Theorem Proving in Higher Order Logics [[electronic resource] ] : 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings / / edited by Klaus Schneider, Jens Brandt |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
|
|
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
Edizione |
[1st ed. 2007.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (VIII, 404 p.) |
|
|
|
|
|
|
Collana |
|
Theoretical Computer Science and General Issues, , 2512-2029 ; ; 4732 |
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Computer science |
Machine theory |
Software engineering |
Artificial intelligence |
Logic design |
Theory of Computation |
Formal Languages and Automata Theory |
Computer Science Logic and Foundations of Programming |
Software Engineering |
Artificial Intelligence |
Logic Design |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
Bibliographic Level Mode of Issuance: Monograph |
|
|
|
|
|
|
Nota di bibliografia |
|
Includes bibliographical references and index. |
|
|
|
|
|
|
Nota di contenuto |
|
On the Utility of Formal Methods in the Development and Certification of Software -- Formal Techniques in Software Engineering: Correct Software and Safe Systems -- Separation Logic for Small-Step cminor -- Formalising Java’s Data Race Free Guarantee -- Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL -- Formalising Generalised Substitutions -- Extracting Purely Functional Contents from Logical Inductive Types -- A Modular Formalisation of Finite Group Theory -- Verifying Nonlinear Real Formulas Via Sums of Squares -- Verification of Expectation Properties for Discrete Random Variables in HOL -- A Formally Verified Prover for the Description Logic |
|
|
|
|
|
|
|
|
|
|
-- Proof Pearl: The Termination Analysis of Terminator -- Improving the Usability of HOL Through Controlled Automation Tactics -- Verified Decision Procedures on Context-Free Grammars -- Using XCAP to Certify Realistic Systems Code: Machine Context Management -- Proof Pearl: De Bruijn Terms Really Do Work -- Proof Pearl: Looping Around the Orbit -- Source-Level Proof Reconstruction for Interactive Theorem Proving -- Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF -- Automatically Translating Type and Function Definitions from HOL to ACL2 -- Operational Reasoning for Concurrent Caml Programs and Weak Memory Models -- Proof Pearl: Wellfounded Induction on the Ordinals Up to ? 0 -- A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols -- Primality Proving with Elliptic Curves -- HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism -- Building Formal Method Tools in the Isabelle/Isar Framework -- Simple Types in Type Theory: Deep and Shallow Encodings -- Mizar’s Soft Type System. |
|
|
|
|
|
| |