The Resource Interactive theorem proving : first international conference, ITP 2010, Edinburgh, UK, July 11-14, 2010 : proceedings, Matt Kaufmann, Lawrence C. Paulsen (eds.), (electronic resource)

Interactive theorem proving : first international conference, ITP 2010, Edinburgh, UK, July 11-14, 2010 : proceedings, Matt Kaufmann, Lawrence C. Paulsen (eds.), (electronic resource)

Label
Interactive theorem proving : first international conference, ITP 2010, Edinburgh, UK, July 11-14, 2010 : proceedings
Title
Interactive theorem proving
Title remainder
first international conference, ITP 2010, Edinburgh, UK, July 11-14, 2010 : proceedings
Statement of responsibility
Matt Kaufmann, Lawrence C. Paulsen (eds.)
Title variation
ITP 2010
Creator
Contributor
Provider
Subject
Genre
Language
eng
Summary
This book constitutes the refereed proceedings of the First International Conference on Interactive Theorem proving, ITP 2010, held in Edinburgh, UK, in July 2010. The 33 revised full papers presented were carefully reviewed and selected from 74 submissions. The papers are organized in topics such as counterexample generation, hybrid system verification, translations from one formalism to another, and cooperation between tools. Several verification case studies were presented, with applications to computational geometry, unification, real analysis, etc
Member of
Cataloging source
GW5XE
Image bit depth
0
LC call number
QA76.9.A96
LC item number
I87 2010
Literary form
non fiction
http://bibfra.me/vocab/lite/meetingDate
2010
http://bibfra.me/vocab/lite/meetingName
ITP (Conference)
Nature of contents
dictionaries
http://library.link/vocab/relatedWorkOrContributorName
  • SpringerLink
  • Kaufmann, Matt
  • Paulson, Lawrence C
Series statement
Lecture Notes in Computer Science,
Series volume
6172
http://library.link/vocab/subjectName
  • Artificial Intelligence
  • Logic
  • Automatic theorem proving
  • Computer logic
  • Automatic theorem proving
  • Computer logic
  • Informatique
Label
Interactive theorem proving : first international conference, ITP 2010, Edinburgh, UK, July 11-14, 2010 : proceedings, Matt Kaufmann, Lawrence C. Paulsen (eds.), (electronic resource)
Instantiates
Publication
Note
International conference proceedings
Antecedent source
mixed
Bibliography note
Includes bibliographical references and author index
Color
not applicable
Contents
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
Dimensions
unknown
Extent
1 online resource (xi, 493 p.)
File format
multiple file formats
Form of item
  • online
  • electronic
Isbn
9783642140525
Level of compression
uncompressed
Other physical details
ill.
Quality assurance targets
absent
Reformatting quality
access
Specific material designation
remote
Stock number
978-3-642-14051-8
System control number
  • (OCoLC)663096303
  • (OCoLC)ocn663096303
Label
Interactive theorem proving : first international conference, ITP 2010, Edinburgh, UK, July 11-14, 2010 : proceedings, Matt Kaufmann, Lawrence C. Paulsen (eds.), (electronic resource)
Publication
Note
International conference proceedings
Antecedent source
mixed
Bibliography note
Includes bibliographical references and author index
Color
not applicable
Contents
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
Dimensions
unknown
Extent
1 online resource (xi, 493 p.)
File format
multiple file formats
Form of item
  • online
  • electronic
Isbn
9783642140525
Level of compression
uncompressed
Other physical details
ill.
Quality assurance targets
absent
Reformatting quality
access
Specific material designation
remote
Stock number
978-3-642-14051-8
System control number
  • (OCoLC)663096303
  • (OCoLC)ocn663096303

Library Locations

  • African Studies LibraryBorrow it
    771 Commonwealth Avenue, 6th Floor, Boston, MA, 02215, US
    42.350723 -71.108227
  • Alumni Medical LibraryBorrow it
    72 East Concord Street, Boston, MA, 02118, US
    42.336388 -71.072393
  • Astronomy LibraryBorrow it
    725 Commonwealth Avenue, 6th Floor, Boston, MA, 02445, US
    42.350259 -71.105717
  • Fineman and Pappas Law LibrariesBorrow it
    765 Commonwealth Avenue, Boston, MA, 02215, US
    42.350979 -71.107023
  • Frederick S. Pardee Management LibraryBorrow it
    595 Commonwealth Avenue, Boston, MA, 02215, US
    42.349626 -71.099547
  • Howard Gotlieb Archival Research CenterBorrow it
    771 Commonwealth Avenue, 5th Floor, Boston, MA, 02215, US
    42.350723 -71.108227
  • Mugar Memorial LibraryBorrow it
    771 Commonwealth Avenue, Boston, MA, 02215, US
    42.350723 -71.108227
  • Music LibraryBorrow it
    771 Commonwealth Avenue, 2nd Floor, Boston, MA, 02215, US
    42.350723 -71.108227
  • Pikering Educational Resources LibraryBorrow it
    2 Silber Way, Boston, MA, 02215, US
    42.349804 -71.101425
  • School of Theology LibraryBorrow it
    745 Commonwealth Avenue, 2nd Floor, Boston, MA, 02215, US
    42.350494 -71.107235
  • Science & Engineering LibraryBorrow it
    38 Cummington Mall, Boston, MA, 02215, US
    42.348472 -71.102257
  • Stone Science LibraryBorrow it
    675 Commonwealth Avenue, Boston, MA, 02445, US
    42.350103 -71.103784
Processing Feedback ...