Interactive Theorem Proving: 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, ProceedingsJeremy Avigad, Assia Mahboubi This book constitutes the refereed proceedings of the 9th International Conference on Interactive Theorem Proving, ITP 2018, held in Oxford, UK, in July 2018. The 32 full papers and 5 short papers presented were carefully reviewed and selected from 65 submissions. The papers feature research in the area of logical frameworks and interactive proof assistants. The topics include theoretical foundations and implementation aspects of the technology, as well as applications to verifying hardware and software systems to ensure their safety and security, and applications to the formal verication of mathematical results.Chapters 2, 10, 26, 29, 30 and 37 are available open access under a Creative Commons Attribution 4.0 International License via link.springer.com. |
Contents
| 1 | |
| 20 | |
Formalizing Ring Theory in PVS | 40 |
Software Tool Support for Modular Reasoning in Modal Logics of Actions | 48 |
Backwards and Forwards with Separation Logic | 68 |
A Coq Formalisation of SQLs Execution Engines | 88 |
A Coq Tactic for Equality Learning in Linear Arithmetic | 108 |
The Coinductive Formulation of Common Knowledge | 126 |
Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB | 362 |
Constructive Extraction of Cycle Finding Algorithms | 370 |
Fast Machine Words in IsabelleHOL | 388 |
Relational Parametricity and Quotient Preservation for Modular Codatatypes | 411 |
Towards Verified Handwritten Calculational Proofs | 432 |
A Formally Verified Solver for Homogeneous Linear Diophantine Equations | 441 |
Formalizing Implicative Algebras in Coq | 459 |
Boosting the Reuse of Formal Specifications | 477 |
Tactics and Certificates in Meta Dedukti | 142 |
A Formalization of the LLL Basis Reduction Algorithm | 160 |
A Formal Proof of the MinorExclusion Property for TreewidthTwo Graphs | 178 |
Verified Analysis of Random Binary Tree Structures | 196 |
HOL Light QE | 215 |
Efficient MendlerStyle LambdaEncodings in Cedille | 235 |
Verification of PCPRelated Computational Reductions in Coq | 253 |
Watchlist Guidance for Large Theories in E | 270 |
Reification by Parametricity | 289 |
Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata | 306 |
A Proof Checker for Teaching the Logical Approach to Discrete Math | 324 |
An Empirical Investigation of KeY | 342 |
Towards Formal Foundations for Game Theory | 495 |
Verified Timing Transformations in Synchronous Circuits with Ware | 504 |
A Formal Equational Theory for CallByPushValue | 523 |
Program Verification in the Presence of Cached Address Translation | 542 |
Verified Tail Bounds for Randomized Programs | 560 |
Verified Memoization and Dynamic Programming | 579 |
Probabilistic Timed Automata Formalized Short Paper | 597 |
Formalization of a Polymorphic Subtyping Algorithm | 604 |
An Agda Formalization of Üresin Dubois Asynchronous FixedPoint Theory | 623 |
Interactive Theorem Proving | 640 |
| 641 | |
Other editions - View all
Interactive Theorem Proving: 9th International Conference, ITP 2018, Held as ... Jeremy Avigad,Assia Mahboubi No preview available - 2018 |
Common terms and phrases
abstract algebra algorithm allows apply approach argument assume assumptions automatically bound calculus called clauses combination complete Comput construction contains context correctness corresponding defined definition dependent derive elements equality equational equivalence evaluation example exists expression formal formula function give given goal graph Heidelberg holds implementation implicative includes induction input introduce Isabelle/HOL knowledge language Lemma LNCS logic method natural Note obtain operations parameters particular predicate present problem proof properties prove random reasoning recursive reduced relation representation represents requires respect returns rules satisfies Sect semantics separation simple solution specification Springer step structure symbols syntax tactic takes term theorem theory tool translation tree University variables verified write