000 | 04631nam a22006135i 4500 | ||
---|---|---|---|
001 | 978-3-642-14052-5 | ||
003 | DE-He213 | ||
005 | 20240730195535.0 | ||
007 | cr nn 008mamaa | ||
008 | 100712s2010 gw | s |||| 0|eng d | ||
020 |
_a9783642140525 _9978-3-642-14052-5 |
||
024 | 7 |
_a10.1007/978-3-642-14052-5 _2doi |
|
050 | 4 | _aQA75.5-76.95 | |
072 | 7 |
_aUYA _2bicssc |
|
072 | 7 |
_aCOM014000 _2bisacsh |
|
072 | 7 |
_aUYA _2thema |
|
082 | 0 | 4 |
_a004.0151 _223 |
245 | 1 | 0 |
_aInteractive Theorem Proving _h[electronic resource] : _bFirst International Conference, ITP 2010 Edinburgh, UK, July 11-14, 2010, Proceedings / _cedited by Matt Kaufmann, Lawrence C. Paulson. |
250 | _a1st ed. 2010. | ||
264 | 1 |
_aBerlin, Heidelberg : _bSpringer Berlin Heidelberg : _bImprint: Springer, _c2010. |
|
300 |
_aXI, 495 p. 82 illus. _bonline resource. |
||
336 |
_atext _btxt _2rdacontent |
||
337 |
_acomputer _bc _2rdamedia |
||
338 |
_aonline resource _bcr _2rdacarrier |
||
347 |
_atext file _bPDF _2rda |
||
490 | 1 |
_aTheoretical Computer Science and General Issues, _x2512-2029 ; _v6172 |
|
505 | 0 | _aInvited Talks -- A Formally Verified OS Kernel. Now What? -- Proof Assistants as Teaching Assistants: A View from the Trenches -- Proof Pearls -- A Certified Denotational Abstract Interpreter -- Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure -- A New Foundation for Nominal Isabelle -- (Nominal) Unification by Recursive Descent with Triangular Substitutions -- A Formal Proof of a Necessary and Sufficient Condition for Deadlock-Free Adaptive Networks -- Regular Papers -- Extending Coq with Imperative Features and Its Application to SAT Verification -- A Tactic Language for Declarative Proofs -- Programming Language Techniques for Cryptographic Proofs -- Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder -- Formal Proof of a Wave Equation Resolution Scheme: The Method Error -- An Efficient Coq Tactic for Deciding Kleene Algebras -- Fast LCF-Style Proof Reconstruction for Z3 -- The Optimal Fixed Point Combinator -- Formal Study of Plane Delaunay Triangulation -- Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison -- A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture -- Automated Machine-Checked Hybrid System Safety Proofs -- Coverset Induction with Partiality and Subsorts: A Powerlist Case Study -- Case-Analysis for Rippling and Inductive Proof -- Importing HOL Light into Coq -- A Mechanized Translation from Higher-Order Logic to Set Theory -- The Isabelle Collections Framework -- Interactive Termination Proofs Using Termination Cores -- A Framework for Formal Verification of Compiler Optimizations -- On the Formalization of the Lebesgue Integration Theory in HOL -- From Total Store Order to Sequential Consistency: A Practical Reduction Theorem -- Equations: A Dependent Pattern-Matching Compiler -- A Mechanically Verified AIG-to-BDD Conversion Algorithm -- Inductive Consequences in the Calculus of Constructions -- Validating QBF Invalidity in HOL4 -- Rough Diamonds -- Higher-Order Abstract Syntax in Isabelle/HOL -- Separation Logic Adapted for Proofs by Rewriting -- Developing the Algebraic Hierarchy with Type Classes in Coq. | |
650 | 0 |
_aComputer science. _99832 |
|
650 | 0 |
_aSoftware engineering. _94138 |
|
650 | 0 |
_aMachine theory. _9160574 |
|
650 | 0 |
_aCompilers (Computer programs). _93350 |
|
650 | 0 |
_aArtificial intelligence. _93407 |
|
650 | 0 |
_aImmunospecificity. _9142719 |
|
650 | 1 | 4 |
_aComputer Science Logic and Foundations of Programming. _942203 |
650 | 2 | 4 |
_aSoftware Engineering. _94138 |
650 | 2 | 4 |
_aFormal Languages and Automata Theory. _9160575 |
650 | 2 | 4 |
_aCompilers and Interpreters. _931853 |
650 | 2 | 4 |
_aArtificial Intelligence. _93407 |
650 | 2 | 4 |
_aAdaptive Immunity. _9142721 |
700 | 1 |
_aKaufmann, Matt. _eeditor. _4edt _4http://id.loc.gov/vocabulary/relators/edt _9160576 |
|
700 | 1 |
_aPaulson, Lawrence C. _eeditor. _4edt _4http://id.loc.gov/vocabulary/relators/edt _9160577 |
|
710 | 2 |
_aSpringerLink (Online service) _9160578 |
|
773 | 0 | _tSpringer Nature eBook | |
776 | 0 | 8 |
_iPrinted edition: _z9783642140518 |
776 | 0 | 8 |
_iPrinted edition: _z9783642140532 |
830 | 0 |
_aTheoretical Computer Science and General Issues, _x2512-2029 ; _v6172 _9160579 |
|
856 | 4 | 0 | _uhttps://doi.org/10.1007/978-3-642-14052-5 |
912 | _aZDB-2-SCS | ||
912 | _aZDB-2-SXCS | ||
912 | _aZDB-2-LNC | ||
942 | _cELN | ||
999 |
_c95671 _d95671 |