Vai al contenuto principale della pagina

Interactive Theorem Proving [[electronic resource] ] : First International Conference, ITP 2010 Edinburgh, UK, July 11-14, 2010, Proceedings / / edited by Matt Kaufmann, Lawrence C. Paulson



(Visualizza in formato marc)    (Visualizza in BIBFRAME)

Titolo: Interactive Theorem Proving [[electronic resource] ] : First International Conference, ITP 2010 Edinburgh, UK, July 11-14, 2010, Proceedings / / edited by Matt Kaufmann, Lawrence C. Paulson Visualizza cluster
Pubblicazione: Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010
Edizione: 1st ed. 2010.
Descrizione fisica: 1 online resource (XI, 495 p. 82 illus.)
Disciplina: 005.1015113
Soggetto topico: Computer science
Software engineering
Machine theory
Compilers (Computer programs)
Artificial intelligence
Immunospecificity
Computer Science Logic and Foundations of Programming
Software Engineering
Formal Languages and Automata Theory
Compilers and Interpreters
Artificial Intelligence
Adaptive Immunity
Persona (resp. second.): KaufmannMatt
PaulsonLawrence C
Note generali: Bibliographic Level Mode of Issuance: Monograph
Nota di bibliografia: Includes bibliographical references and index.
Nota di contenuto: Invited 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.
Titolo autorizzato: Interactive Theorem Proving  Visualizza cluster
ISBN: 1-280-38759-9
9786613565518
3-642-14052-1
Formato: Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione: Inglese
Record Nr.: 996465785003316
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Serie: Theoretical Computer Science and General Issues, . 2512-2029 ; ; 6172