Interactive Theorem Proving

Name: Interactive Theorem Proving | 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings
Brand: Springer
Price: 96.29 EUR
Availability: OnlineOnly

9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings

Jeremy Avigad Assia Mahboubi(Editor)

Springer (Publisher)

Published on 3. July 2018

XVII, 642 pages

E-Book

PDF with digital watermarking

System requirements

978-3-319-94821-8 (ISBN)

€96.29incl. 7% vat

System requirements

for PDF with digital watermarking

E-Book Single Licence

Available for download

Description

More details

Other editions

Content

Intro
Preface
Organization
Abstracts of Invited Talks
Deductive Program Verification
Voevodsky's Work on Formalization of Proofs and the Foundations of Mathematics
Mike Gordon: Tribute to a Pioneer in Theorem Proving and Formal Verification
Contents
Physical Addressing on Real Hardware in Isabelle/HOL
1 Introduction
2 Model
2.1 Views and Termination
2.2 Concrete Syntax, Prolog, and Sockeye
2.3 View-Equivalence and Refinement
3 Refinement: Example of the MIPS R4600 TLB
3.1 The TLB Model
3.2 The Validity Invariant
3.3 Invariant Violation at Power On
3.4 What Does a Fully-Wired TLB Do?
3.5 The TLB Refines a Decoding Net
3.6 Modeling TLB Lookups and Exceptions
3.7 Adding a Page Table
3.8 Modeling Replacement Handlers
3.9 Equivalence to Infinitely Large TLB
4 Conclusion
References
Towards Certified Meta-Programming with Typed Template-Coq
1 Introduction
2 Reification of Coq Terms
3 Type Checking Coq in Coq
4 Reification of Coq Commands
5 Writing Coq Plugins in Coq
5.1 A Plugin to Add a Constructor
5.2 Parametricity Plugin
5.3 Intensional Function Plugin
6 Related Work and Future Work
References
Formalizing Ring Theory in PVS
1 Introduction
2 The theory rings: Formalized so Far
2.1 The subtheory ring_general_results
2.2 The subtheory finite_integral_domain
2.3 The subtheory ring_binomial_theorem
2.4 The subtheory ring_isomorphism_theorems
3 Related Work
4 Conclusions and Future Work
References
Software Tool Support for Modular Reasoning in Modal Logics of Actions
1 Introduction
2 Display Calculi and D.EAK
3 The D.EAK Calculus Toolbox
3.1 Shallow Embedding (SE) in Isabelle
3.2 Deep Embedding (DE) in Isabelle
3.3 Functionality of the User Interface (UI)
4 Case Study: The Muddy Children Puzzle
4.1 The Muddy Children Puzzle
4.2 Muddy Children in Isabelle
4.3 Conclusions from the Case Study
5 Meta-toolbox - Building Your Own Calculus Toolbox
5.1 Describing a Calculus
5.2 The Build Script, the Template Files, and the Watcher Utility
6 Conclusion
References
Backwards and Forwards with Separation Logic
1 Introduction
2 Notation
3 Hoare Logic and Separation Logic
4 Separating Coimplication
5 Walking Backwards
6 Walking Forwards
7 Related Work
8 Summary
References
A Coq Formalisation of SQL's Execution Engines
1 Introduction
2 SQL's Compilation in a Nutshell
3 A High-Level Specification for Data-Centric Operators
4 Physical Algebra
4.1 Iterators
4.2 Index-Based Operators
4.3 Adequacy
5 SQL Algebra
5.1 Syntax and Semantics
5.2 Adequacy
6 Formally Bridging Logical and Physical Algebra
7 Related Works, Lessons, Conclusions and Perspectives
References
A Coq Tactic for Equality Learning in Linear Arithmetic
1 Introduction
2 Specification of the VPL Tactic
2.1 The Three Steps of the Tactic
2.2 The Proof Built by the Tactic
3 Using the vpl Tactic
4 The Witness Format in the Tactic
4.1 Certified Farkas Operations
4.2 Example of Proof Witness
4.3 The HOAS of Proof Witnesses
5 The Reduction Algorithm
5.1 A Refined Specification of the Reduction
5.2 Building Equality Witnesses from Conflicts
5.3 Illustration on the Running Example
5.4 Description of the Algorithm
6 Conclusion and Related Works
References
The Coinductive Formulation of Common Knowledge
1 Introduction
2 Possible Worlds and Events
3 Knowledge Operator Semantics
4 Relational Semantics
5 Equivalence with Relational Common Knowledge
6 Conclusion
References
Tactics and Certificates in Meta Dedukti
1 Introduction
2 First-Order Logic in Dedukti
3 A Typed Tactic Language for Meta Dedukti
4 An Untyped Tactic Language for Meta Dedukti
5 Example of Interactive Proof Development
6 Theorem Transfer
7 Resolution Certificates
8 Related Works
9 Conclusion
References
A Formalization of the LLL Basis Reduction Algorithm
1 Introduction
2 Preliminaries
3 Gram-Schmidt Orthogonalization
4 The LLL Basis Reduction Algorithm
5 Experimental Evaluation of the Verified LLL Algorithm
6 Factorization of Polynomials in Polynomial Time
6.1 Short Vectors for Polynomial Factorization
6.2 Bug in Modern Computer Algebra
6.3 A Verified Factorization Algorithm
7 Summary
References
A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs
1 Introduction
2 Simple Graphs
3 Treewidth and Minors
4 Graphs
5 Checkpoints
6 Extracting Terms from K4-free Graphs
7 Isomorphism Properties
8 Conclusion
References
Verified Analysis of Random Binary Tree Structures
1 Introduction
2 Probability Theory in Isabelle/HOL
2.1 Measures and Probability Mass Functions
2.2 The Giry Monad
3 Quicksort
3.1 Randomised Quicksort
3.2 Average-Case of Non-randomised Quicksort
4 Random Binary Search Trees
4.1 Preliminaries
4.2 Internal Path Length
4.3 Height
5 Treaps
5.1 Definition
5.2 The Measurable Space of Trees
5.3 Randomisation
6 Related Work
7 Future Work
References
HOL Light QE
1 Introduction
2 CTTqe
2.1 Syntax
2.2 Semantics
2.3 Quasiquotation
2.4 Proof System
2.5 The Three Design Problems
3 HOL Light
4 Implementation
4.1 Overview
4.2 Mapping of CTTqe Expressions to HOL Terms
4.3 Modification of the HOL Light Proof System
4.4 Creation of Support Machinery
4.5 Metatheorems
5 Examples
5.1 Law of Excluded Middle
5.2 Induction Schema
6 Related Work
7 Conclusion
References
Efficient Mendler-Style Lambda-Encodings in Cedille
1 Introduction
2 Background
3 Preliminaries
3.1 Multiple Types of Terms
3.2 Identity Functions
3.3 Identity Mapping
4 Inductive Datatypes from Identity Mappings
4.1 Basics of Mendler-Style Encoding
4.2 Inductive Subset
4.3 Induction Principle
5 Constant-Time Destructors
5.1 Constant-Time Destructor for Mendler-Style Encoding
6 Examples
6.1 Natural Numbers with Constant-Time Predecessor
6.2 Infinitary Trees
6.3 Unbalanced Trees
7 Related Work
8 Conclusions and Future Work
References
Verification of PCP-Related Computational Reductions in Coq
1 Introduction
2 Definitions
2.1 Post Correspondence Problem
2.2 String Rewriting
2.3 Post Grammars
2.4 Alphabets
2.5 Freshness
3 SRH to SR
4 SR to MPCP
5 MPCP to PCP
6 PCP to CFP
7 PCP to CFI
8 TM to SRH
9 Discussion
References
ProofWatch: Watchlist Guidance for Large Theories in E
1 Introduction: Hammers, Learning and Watchlists
2 Proof Search in Saturating First-Order Provers
3 Proof Search State in Learning Based Guidance
3.1 Proof Search State Representation for Guiding Saturation
4 Static Watchlist Guidance and Its Implementation in E
5 Dynamic Watchlist Guidance
5.1 Watchlist Proof Progress
5.2 Standard Dynamic Watchlist Relevance
5.3 Inherited Dynamic Watchlist Relevance
6 Experiments with Watchlist Guidance
6.1 Watchlist Selection Methods
6.2 Using Watchlists in E Strategies
6.3 Evaluation
7 Examples
8 Related Work and Possible Extensions
8.1 Possible Extensions
9 Conclusion
References
Reification by Parametricity
1 Introduction
1.1 Proof-Script Primer
1.2 Reflective-Automation Primer
1.3 Reflective-Syntax Primer
2 Methods of Reification
3 Reification by Parametricity
3.1 Case-By-Case Walkthrough
3.2 Commuting Abstraction and Reduction
3.3 Implementation in Ltac
3.4 Advantages and Disadvantages
4 Performance Comparison
4.1 Without Binders
4.2 With Binders
5 Future Work, Concluding Remarks
References
Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata
1 Introduction
2 Preliminaries
2.1 Linear Temporal Logic
2.2 Co-Büchi Alternating Automata
2.3 Generalized Büchi Automata
3 Translating LTL to GBA
4 Verifying the Algorithm
4.1 Mechanizing the Abstract Proofs
4.2 Concrete Data Structures
4.3 Abstraction Functions
4.4 Concrete Translations
4.5 Verifying the Concrete Functions
5 Related Work
6 Conclusion
References
CALCCHECK: A Proof Checker for Teaching the ``Logical Approach to Discrete Math''
1 Introduction
2 The Basic CALCCHECK Language
3 The CALCCHECKWeb Front-End
4 Structured Proofs
5 Quantification, Substitution, Metavariables
6 Combined Hint Items
6.1 Conditional Rewriting
6.2 Rule Transformation
6.3 Theorems as Proof Methods - ``Using''
7 Activation of Features
8 Implementation Aspects
9 Discussion of Related Work
10 Conclusion
References
Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY
1 Introduction
2 Problem Statement
3 Parameters of Deductive Verification with KeY
4 Empirical Evaluation of KeY's Parameters
4.1 Experimental Setup
4.2 Empricial Evaluation of Assumptions
4.3 Learning a Parameter-Influence Model
4.4 Threats to Validity
5 Suggestions for Users and Tool Builders
6 Related Work
7 Conclusion
References
Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB
1 Introduction
2 Binary Code Extraction Workflow
3 Trusted Computing Base
4 Broader Context and Vision
References
Proof Pearl: Constructive Extraction of Cycle Finding Algorithms
1 Introduction
2 Formalization of the Problem
2.1 An OCaml Account of the Tortoise and the Hare
2.2 Goals and Contributions
3 Termination Using Bar Inductive Predicates
3.1 Dependently Typed Recursion for Bar Inductive Predicates
3.2 Accessibility vs. Bar Inductive Predicates
3.3 Constructive Epsilon via Bar Inductive Predicates
4 The Tortoise and the Hare via Bar Inductive Predicates
4.1 A Non-tail Recursive Implementation
4.2 A Tail-Recursive Implementation
5 Floyd's Cycle Finding Algorithm in Coq
5.1 Computing a Meeting Point
5.2 Computing the Index
5.3 Computing the Period
5.4 Gluing all Together
6 Brent's Period Finding Algorithm
7 Correctness by Extraction and Related Works
7.1 Correctness of the Tortoise and the Hare
7.2 Comparison with Related Works
References
Fast Machine Words in Isabelle/HOL
1 Introduction
2 Background on Isabelle/HOL
3 Fixed-Size Machine Words
3.1 Types of Unsigned Words
3.2 Setting up Code Generation
3.3 Dealing with Underspecification
3.4 Soundness of Code Adaptations for Underspecified HOL Functions
4 Machine Words of Unspecified Length
5 Validation
5.1 Automating Regression Tests for Code Generation
5.2 Test Case Selection and Validation Results
6 Evaluation
7 Related Work
8 Conclusion and Future Work
References
Relational Parametricity and Quotient Preservation for Modular (Co)datatypes
1 Introduction
1.1 Background: Bounded Natural Functors
1.2 Examples and Applications
2 Bounded Natural Functors with Co- and Contravariance
3 Simple Operations on BNFCCs
4 Least and Greatest Fixpoints
5 Subtypes
6 Quotient Preservation
7 Related Work
8 Conclusion and Future Work
References
Towards Verified Handwritten Calculational Proofs
1 Introduction
2 Background and Related Work
3 Requirements
4 Proof-of-Concept Prototype
5 Conclusion and Future Work
References
A Formally Verified Solver for Homogeneous Linear Diophantine Equations
1 Introduction
2 Main Ideas
3 An Isabelle/HOL Theory of HLDEs and Their Solutions
4 Certified Minimal Complete Sets of Solutions
5 Special and Non-special Solutions
6 A More Efficient Algorithm for Code Generation
7 Evaluation
8 Related Work
9 Conclusions and Further Work
References
Formalizing Implicative Algebras in Coq
1 Introduction
2 Krivine Classical Realizability
3 Implicative Structures
3.1 Definition
3.2 Examples of Implicative Structures
4 Interpreting the -calculus
4.1 Interpretation of -terms
4.2 Adequacy
4.3 Combinators
4.4 The Problem of Consistency
5 Implicative Algebras
5.1 Separation
5.2 c-terms
5.3 Internal Logic
5.4 Implicative Tripos
6 Conclusion and Future Work
6.1 Conclusion
6.2 Future Work
References
Boosting the Reuse of Formal Specifications
1 Introduction
2 Preliminary Definitions
3 Representation Technique
4 Case Study
5 Related Work
6 Conclusion
References
Towards Formal Foundations for Game Theory
1 Introduction
2 Isabelle/HOL, Probability, and Notations
3 Preference Relations and Their Properties
4 The Setup
5 The Proof Outline
6 Conclusions
References
Verified Timing Transformations in Synchronous Circuits with -Ware
1 Introduction
2 Overview
3 -Ware
4 Semantics and Properties
5 Combinational and Sequential Combinators
5.1 Convertibility of Combinational and Sequential Versions
5.2 Applications of the Combinational and Sequential Combinators
6 Discussion
6.1 Related Work
6.2 Future Work
7 Conclusion
References
A Formal Equational Theory for Call-By-Push-Value
1 Introduction
2 The Pure Untyped Call-by-Value -calculus
2.1 Progress and Canonical Forms
2.2 Contextual Equivalence
2.3 Equational Theory
2.4 Soundness of the Equational Theory for CBV
3 A Call-by-Push-Value Language
3.1 Syntax
3.2 Wellformedness
3.3 Structural Operational Semantics
3.4 Progress, and Canonical and Error Forms
3.5 Contextual Equivalence
3.6 Equational Theory
3.7 Soundness of the Equational Theory for CBPV
4 Verifying Optimizations Using Our Equational Theory
5 Conclusion and Future Work
A Appendix: Definition of P for CBPV
References
Program Verification in the Presence of Cached Address Translation
1 Introduction
2 Related Work
3 Notation
4 Logic
4.1 Syntax and Program State
4.2 Semantic Operations
4.3 Hoare Logic
4.4 Discussion
5 Safe Set
6 Case Studies
6.1 User Execution
6.2 Kernel Execution
6.3 Context Switch
7 Summary
References
Verified Tail Bounds for Randomized Programs
1 Introduction
2 Probability Preliminaries
2.1 Discrete Probability
2.2 Monadic Encoding
3 Karp's Theorem
3.1 Unary Recurrences
3.2 Extension to Binary Work and Span Recurrences
4 Examples
4.1 Sequential QuickSort
4.2 Other Examples
5 Changes Needed for Mechanization
5.1 Overview of Proof
5.2 Changes
6 Related Work
6.1 Verification of Randomized Algorithms and Mechanized Probability Theory
6.2 Techniques for Bounds on Randomized Algorithms
7 Conclusion
References
Verified Memoization and Dynamic Programming
1 Introduction
1.1 Related Work
2 Memoization
2.1 Overview
2.2 Monadification
2.3 Reasoning with Parametricity
2.4 Termination
2.5 Technical Limitations
2.6 Memoization
2.7 Imperative Memoization
2.8 Bottom-up Computation
2.9 Memory Implementations
3 Examples
3.1 Bellman-Ford Algorithm
3.2 Knapsack Problem
3.3 A Counting Problem
3.4 The Cocke-Younger-Kasami Algorithm
3.5 Minimum Edit Distance
4 Future Work
References
MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper)
1 Introduction
2 Preliminaries
3 Probabilistic Timed Automata
4 Bisimulation
5 Taking Zenoness into Account
6 Conclusion
References
Formalization of a Polymorphic Subtyping Algorithm
1 Introduction
2 Overview: Polymorphic Subtyping
2.1 Declarative Polymorphic Subtyping
2.2 Finding Solutions for Variable Instantiation
2.3 The Worklist Approach
3 A Worklist Algorithm for Polymorphic Subtyping
3.1 Syntax and Well-Formedness of the Algorithmic System
3.2 Algorithmic Subtyping
4 Metatheory
4.1 Transfer to the Declarative System
4.2 Soundness
4.3 Completeness
4.4 Decidability
5 The Choice of Abella
5.1 Statistics and Discussion
6 Related Work
7 Conclusion and Future Work
References
An Agda Formalization of Üresin & Dubois' Asynchronous Fixed-Point Theory
1 Introduction
2 Preliminaries
2.1 Schedules
3 Convergence Theorem
4 The Library
4.1 Synchronous Iteration Conditions
4.2 Finite Conditions
4.3 Ultrametrics
5 Conclusion
References
Erratum to: Interactive Theorem Proving
Erratum to: J. Avigad and A. Mahboubi (Eds.): Interactive Theorem Proving, LNCS 10895, https://doi.org/10.1007/978-3-319-94821-8
Author Index

System requirements

Save as PDF Copy link into clipboard

Schweitzer Fachinformationen

Interactive Theorem Proving

Description

More details

Other editions

Additional editions

Content

System requirements