1 option
Interactive Theorem Proving : 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013, Proceedings / edited by Sandrine Blazy, Christine Paulin-Mohring, David Pichardie.
SpringerLink Books Lecture Notes In Computer Science (LNCS) (1997-2024) Available online
View online- Format:
- Book
- Series:
- Computer Science (Springer-11645)
- LNCS sublibrary. Theoretical computer science and general issues ; SL 1, 7998.
- Theoretical Computer Science and General Issues ; 7998
- Language:
- English
- Subjects (All):
- Logic, Symbolic and mathematical.
- Artificial intelligence.
- Computer logic.
- Software engineering.
- Computer security.
- Algorithms.
- Mathematical Logic and Formal Languages.
- Artificial Intelligence.
- Logics and Meanings of Programs.
- Software Engineering.
- Systems and Data Security.
- Algorithm Analysis and Problem Complexity.
- Local Subjects:
- Mathematical Logic and Formal Languages.
- Artificial Intelligence.
- Logics and Meanings of Programs.
- Software Engineering.
- Systems and Data Security.
- Algorithm Analysis and Problem Complexity.
- Physical Description:
- 1 online resource (XII, 498 pages) : 73 illustrations.
- Edition:
- First edition 2013.
- Contained In:
- Springer eBooks
- Place of Publication:
- Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2013.
- System Details:
- text file PDF
- Summary:
- This book constitutes the refereed proceedings of the 4th International Conference on Interactive Theorem Proving, ITP 2013, held in Rennes, France, in July 2013. The 26 regular full papers presented together with 7 rough diamond papers, 3 invited talks, and 2 invited tutorials were carefully reviewed and selected from 66 submissions. The papers are organized in topical sections such as program verfication, security, formalization of mathematics and theorem prover development.
- Contents:
- Invited Talks
- Applying Formal Methods in the Large
- Automating Theorem Proving with SMT
- Certifying Voting Protocols
- Invited Tutorials.-Counterexample Generation Meets Interactive Theorem Proving: Current Results and Future Opportunities
- Canonical Structures for the Working Coq User
- Regular Papers
- MaSh: Machine Learning for Sledgehammer
- Scalable LCF-Style Proof Translation
- Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation
- Automatic Data Refinement
- Data Refinement in Isabelle/HOL
- Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable
- Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω1
- Mechanising Turing Machines and Computability Theory in Isabelle/HOL.-A Machine-Checked Proof of the Odd Order Theorem
- Kleene Algebra with Tests and Coq Tools for while Programs.-Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL
- Pragmatic Quotient Types in Coq
- Mechanical Verification of SAT Refutations with Extended Resolution
- Formalizing Bounded Increase
- Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types
- Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
- Formal Reasoning about Classified Markov Chains in HOL
- Practical Probability: Applying pGCL to Lattice Scheduling
- Adjustable References
- Handcrafted Inversions Made Operational on Operational Semantics
- Circular Coinduction in Coq Using Bisimulation-Up-To Techniques
- Program Extraction from Nested Definitions
- Subformula Linking as an Interaction Method
- Automatically Generated Infrastructure for De Bruijn Syntaxes
- Shared-Memory Multiprocessing for Interactive Theorem Proving
- A Parallelized Theorem Prover for a Logic with Parallel Execution
- Rough Diamonds
- Communicating Formal Proofs: The Case of Flyspeck
- Square Root and Division Elimination in PVS
- The Picard Algorithm for Ordinary Differential Equations in Coq
- Stateless Higher-Order Logic with Quantified Types
- Implementing Hash-Consed Structures in Coq
- Towards Certifying Network Calculus
- Steps towards Verified Implementations of HOL Light.
- Other Format:
- Printed edition:
- ISBN:
- 978-3-642-39634-2
- 9783642396342
- Access Restriction:
- Restricted for use by site license.
The Penn Libraries is committed to describing library materials using current, accurate, and responsible language. If you discover outdated or inaccurate language, please fill out this feedback form to report it and suggest alternative language.