Interactive Theorem Proving

Name: Interactive Theorem Proving | 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings

Jasmin Christian Blanchette Stephan Merz(Herausgeber*in)

Springer (Verlag)

Erschienen am 8. August 2016

XVII, 502 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-319-43144-4 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

Intro
Preface
Organization
Abstracts of Keynote Presentations
Propositions as Programs, Proofs as Programs
Formal Verification of Financial Algorithms, Progress and Prospects
Dijkstra Monads for Free: A Framework for Deriving and Extending F*'s Effectful Semantics
Contents
Regular Contributions
An Isabelle/HOL Formalisation of Green's Theorem
1 Introduction
2 Basic Concepts and Lemmas
3 More General Structures
3.1 Chains and Cubes
3.2 Dealing with Boundaries
4 Conclusion and Future Work
References
HOL Zero's Solutions for Pollack-Inconsistency
1 Introduction
1.1 Overview
1.2 Concepts, Terminology and Notation
2 The Need for Good Parsers and Printers
2.1 Proof Auditing
2.2 Usability
3 Classic Problems with HOL Parsers and Printers
3.1 Entities with Irregular Names
3.2 Entities with Keyword Names
3.3 Variable-Constant Overloading
3.4 Variable-Variable Overloading
3.5 Type Ambiguity in Printed Terms
3.6 Juxtaposition of Lexical Tokens in Printed Expressions
4 Lexical Solutions
4.1 Identifier Delimiters
4.2 Variable Marking
4.3 Spacing Between Tokens
5 Type Inference for Variable-Variable Overloading
5.1 Hindley-Milner Type Inference
5.2 A New Notion of Syntactic Scope for Variables
5.3 Adjustments to the Hindley-Milner Algorithm
6 Minimal Unambiguous Type Annotation
7 Conclusions
References
Infeasible Paths Elimination by Symbolic Execution Techniques
1 Introduction
2 Background: Isabelle and Isabelle/HOL
3 A Guided Run of ATRACER
3.1 Presenting ATRACER by an Example
4 The Formalization of ATRACER
4.1 The Theory of Red-Black Graphs
4.2 Graph-Transformations on Red-Black Graphs
4.3 Main Theorems of ATRACER
4.4 Summary
5 Conclusion
References
Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency
1 Introduction
2 Background and Big Picture
3 The Model
3.1 A Generic Model of Interrupt-Driven Interleaving
3.2 Instantiation to the eChronos OS
4 Proof Framework and Scheduler Proof
4.1 Framework and Compositionality Lemma
4.2 The Statement and Its Proof
4.3 Proof-Engineering Considerations
5 Related Work
6 Conclusion
References
POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl)
1 Introduction
2 Preliminaries
3 POSIX Regular Expression Matching
4 Extensions and Optimisations
5 The Correctness Argument by Sulzmann and Lu
6 Conclusion
References
CoSMed: A Confidentiality-Verified Social Media Platform
1 Introduction
2 System Description
2.1 Isabelle Specification
2.2 Implementation
3 Stating Confidentiality
3.1 From CoCon to CoSMed
3.2 BD Security Recalled
3.3 CoSMed Confidentiality as BD Security
3.4 More Confidentiality Properties
4 Verifying Confidentiality
4.1 BD Unwinding Recalled
4.2 Unwinding Relations for CoSMed
5 Verification Summary
6 Related Work
References
Mechanical Verification of a Constructive Proof for FLP
1 Introduction
2 Preliminaries
2.1 Distributed Systems and Consensus
2.2 Isabelle/HOL
3 Model
3.1 Asynchronous System
3.2 Executions
4 FLP Formalization
4.1 FLPSystem
4.2 FLPTheorem
4.3 Proof Structure
4.4 Discussion
5 Conclusion
References
Visual Theorem Proving with the Incredible Proof Machine
1 Introduction
2 Proof Graphs
2.1 Conclusion and Assumption
2.2 Rule Blocks
2.3 Local Hypotheses
2.4 Predicate Logic
2.5 Helper Block
2.6 Custom Blocks
2.7 Custom Logics
3 Theory
3.1 Port Graphs
3.2 Scopes
3.3 Graph Shapes
3.4 Propositions
3.5 Scoped Variables
3.6 Example
3.7 Proof Conclusions
4 Implementation
5 Evaluation
5.1 Classroom Experience
5.2 Online Reception
6 Future Directions
7 Related Work
8 Conclusions
References
Proof Pearl: Bounding Least Common Multiples with Triangles
1 Introduction
2 Background
2.1 LCM Lower Bound for a List
2.2 Pascal's Triangle
2.3 Leibniz's Harmonic Triangle
3 Leibniz's Denominator Triangle and Its Triplets
3.1 LCM Exchange
4 Paths Through Triangles
4.1 Zig-Zag Paths
4.2 Wriggle Paths
4.3 Wriggling Inductions
5 LCM Lower Bound
6 Conclusion
References
Two-Way Automata in Coq
1 Introduction
2 Type Theory Preliminaries
3 Languages in Type Theory
4 One-Way Automata
5 Classifiers and Myhill-Nerode
6 Two-Way Finite Automata
7 Vardi Construction
8 Shepherdson Construction
9 Conclusion
References
Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms
1 Introduction
1.1 Related Work
2 Verifying Stencil Code
2.1 Stencils and Their Representation
2.2 Programs: Syntax, Semantics, and Correctness
2.3 Verification Conditions and Symbolic Execution
3 Verifying Distributed Stencil Algorithms
3.1 Reduction to the Sequential Case
3.2 Distributed Kernels: Syntax, Semantics, and Correctness
3.3 Trace Generation
4 Implementation and Experimental Results
4.1 A Simple Example
4.2 Automation: Sets and Nonlinear Arithmetic
4.3 More Examples
5 Conclusions and Future Work
References
The Flow of ODEs
1 Introduction
2 Overview
3 The Flow of a Differential Equation
3.1 Composition of Solutions
3.2 Continuity of the Flow
3.3 Differentiability of the Flow
4 Rigorous Numerics for the Derivative of the Flow
5 Uniform Limit as Filter
6 Bounded Linear Functions
6.1 Type Classes for Mathematics in Isabelle/HOL
6.2 A Type of Bounded Linear Functions
6.3 Instantiations
6.4 Applications
7 Proofs About the Flow
7.1 Criteria for Unique Solution
7.2 The Frontier of the State Space
7.3 Continuity of the Flow
7.4 Differentiability of the Flow
7.5 Continuity of Derivative
8 Conclusion
References
From Types to Sets by Local Type Definitions in Higher-Order Logic
1 Motivation
2 HOL and Isabelle/HOL Recalled
2.1 Core Logic
2.2 Definitional Mechanisms of HOL
2.3 Definitional Mechanisms of Isabelle/HOL
3 Proposal of a Logic Extension: Local Typedef
4 From Types to Sets in HOL
5 From Types to Sets in Isabelle/HOL
5.1 Local Axiomatic Type Classes
5.2 Local Overloading
5.3 Example: Relativization of Topological Spaces
5.4 General Case
6 Transfer: Automated Relativization
7 Conclusion
References
Formalizing the Edmonds-Karp Algorithm
1 Introduction
2 The Ford-Fulkerson Method
3 Formalizing the Ford-Fulkerson Method
3.1 Presentation of Proofs
3.2 Presentation of Algorithms
4 Refinement in Isabelle/HOL
5 The Edmonds-Karp Algorithm
6 Refinement to Executable Code
6.1 Using Breadth First Search
6.2 Manipulating Residual Graphs Directly
6.3 Implementing Augmentation
6.4 Computing Successors
6.5 Using Efficient Data Structures
6.6 Network Checker
7 Benchmarking
8 Conclusion
8.1 Related Work
8.2 Future Work
References
A Formal Proof of Cauchy's Residue Theorem
1 Introduction
2 Background
2.1 Contour Integrals
2.2 Valid Path
2.3 Winding Number
2.4 Holomorphic Functions and Cauchy's Integral Theorem
2.5 Remarks on the Porting Efforts
3 Cauchy's Residue Theorem
3.1 Residue
3.2 Generalization to a Finite Number of Singularities
3.3 Applications
3.4 Remarks on the Formalization
4 The Argument Principle
4.1 Zeros and Poles
4.2 The Main Proof
4.3 Remarks
5 Rouché's Theorem
6 Related Work
7 Conclusion
References
Equational Reasoning with Applicative Functors
1 Introduction
1.1 Background on Applicative Functors
1.2 Motivating Example: Tree Labelling
2 Modelling Applicative Functors in HOL
3 Lifting with Applicative Functors
3.1 Conversion to Canonical Form
3.2 Lifting
4 Combinators
4.1 The Combinatorial Basis BCKW
4.2 Characterisation of Liftable Equations
4.3 Implementation via Bracket Abstraction
4.4 Application: The Stern-Brocot Tree
5 Related Work
6 Conclusion and Future Work
A Definitions of Applicative Functors
References
Formally Verified Approximations of Definite Integrals
1 Introduction
2 Preliminaries
2.1 Notations and First Definitions
2.2 Elementary Real Analysis in Coq
2.3 Numerical Computations in Coq
3 Interval Methods to Approximate an Integral
3.1 Naive Integral Enclosure
3.2 Polynomial Approximation
3.3 Quality of the Integral Enclosures
3.4 Dichotomy and Adaptivity
4 Automating the Proof Process
4.1 Straight-Line Programs and Enclosures
4.2 Checking Integrability
4.3 Integration into a Tactic
4.4 Controlling the Tactic
5 Benchmarks
6 Conclusion
References
Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems
1 Introduction
2 Preliminaries
3 Strongly Closed Critical Pairs
4 Parallel Closed Critical Pairs
5 Almost Parallel Closed Critical Pairs and Commutation
6 Certification and Experiments
7 Conclusion
References
Automatic Functional Correctness Proofs for Functional Search Trees
1 Introduction
2 Lists and Trees
3 Set Implementations
3.1 The Standard Approach
3.2 The inorder Approach
4 The Verification Framework
4.1 Proof Automation by Rewriting
5 An Arboretum
5.1 Unbalanced Trees
5.2 AVL Trees
5.3 Red-Black Trees
5.4 2-3 Trees
5.5 2-3-4 Trees
5.6 1-2 Brother Trees
5.7 AA Trees
5.8 Splay Trees
6 Maps
6.1 Specifications
6.2 Proof Automation
7 Conclusion
References
A Framework for the Automatic Formal Verification of Refinement from Cogent to C
1 Introduction
2 Overview and Background
2.1 COGENT
2.2 AutoCorres and C Monads in Isabelle/HOL
3 Refinement Framework
3.1 Refinement Statement
3.2 Data Relations
3.3 Refinement Theorem
3.4 Refinement Proof
4 Related Work
5 Take Away Lessons and Future Work
6 Conclusions
References
Formalization of the Resolution Calculus for First-Order Logic
1 Introduction
2 Overview
3 Clausal First-Order Logic
4 The Resolution Calculus
5 Herbrand Interpretations
5.1 Semantic Trees
5.2 Herbrand's Theorem
6 Completeness
6.1 Lifting Lemma
6.2 The Formal Completeness Proof
6.3 Standardizing Apart
6.4 Branches and Ground Clauses
6.5 The Derivation
7 Related Work
8 Conclusion
References
Verified Operational Transformation for Trees
1 Introduction
2 Formalization of OT Algorithms and Their Correctness Properties
2.1 Operation Model
2.2 Transformation of Composite Operations (file Comp.v)https://github.com/JetBrains/ot-coq/blob/master/Comp.v.
3 Examples of Verified Transformation Functions
3.1 The Case of Ordered Trees with Labels
3.2 The Case of Unordered Trees
4 Related Work
5 Conclusions and Future Work
References
Hereditarily Finite Sets in Constructive Type Theory
1 Introduction
2 Preliminaries
3 HF Structures
4 Categoricity
5 Set Operations
6 Ordinals
7 Cardinality
8 Binary Trees
9 Tree Model
10 Conclusion
References
Algebraic Numbers in Isabelle/HOL
1 Introduction
2 Resultants
2.1 Resultant Has Desired Roots
2.2 Resultant Is Non-Zero
3 Euclid-Like Computation of Resultants
3.1 The Algorithm and Its Correctness
3.2 Polynomial Division in Isabelle's Class Hierarchy
3.3 Performance Issues
4 Factorization of Rational Polynomials
4.1 Verified Kronecker's Factorization
4.2 Factorization Oracles
5 Real Algebraic Numbers
5.1 Separation of Roots
5.2 Comparisons of Algebraic Numbers
5.3 Types for Real Algebraic Numbers
6 Complex Algebraic Numbers
7 Displaying Algebraic Numbers
8 Conclusion
References
Modular Dependent Induction in Coq, Mendler-Style
1 Introduction
2 Initial Semantics and Impredicative Encoding
3 Modular Datatypes: An Example
4 Inductive Proofs with MTC Induction
5 Mendler-Style Induction
6 Conclusion
References
Formalized Timed Automata
1 Introduction
1.1 History and Related Work
2 Diagonal-Free Timed Automata in Isabelle/HOL
2.1 Syntactic Definition
2.2 Operational Semantics
2.3 Zone Semantics
3 Difference Bound Matrices
3.1 Fundamentals
3.2 Operations
3.3 DBM Operational Semantics
4 From Classic Decidability to a Correct Approximation
4.1 Regions
4.2 Decidability with Regions
4.3 Approximating Zone Semantics with Regions
5 Normalization
5.1 -approximation
5.2 Connecting Approx and Closure
5.3 Computing Approx
5.4 A Final Semantics
6 Conclusion
References
AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic
1 Introduction
2 Objectives
3 Description of the System
3.1 Box Lattice
3.2 Item Types
3.3 Skolemization and Induction
3.4 Matching
3.5 Scoring
3.6 A Simple Example
3.7 Proof Scripts
3.8 Practical Usage
4 Case Studies
4.1 Elementary Theory of Prime Numbers
4.2 Verification of Imperative Programs
5 Related Work
6 Conclusion
References
Rough Diamonds
What's in a Theorem Name?
1 Introduction
2 Parts of Names and Theorems
3 Learning Associations Between Names and Statements
4 Preliminary Evaluation
5 Conclusions
References
Cardinalities of Finite Relations in Coq
1 Introduction
2 Preliminaries
3 Relation Algebra in Coq
4 Applications
4.1 Linear Orders
4.2 Independence Number of a Graph
5 Conclusion
References
Formalising Semantics for Expected Running Time of Probabilistic Programs
1 Introduction
2 Preliminaries
3 Probabilistic Guarded Command Language (pGCL)
4 Simple Symmetric Random Walk
5 Coupon Collector
6 Related Work
7 Conclusion and Future Work
References
On the Formalization of Fourier Transform in Higher-order Logic
1 Introduction
2 Formalization of Fourier Transform
3 Formal Verification of Fourier Transform Properties
4 Application: Automobile Suspension System
5 Conclusions
References
CoqPIE: An IDE Aimed at Improving Proof Development Productivity
1 Introduction
2 An Overview of CoqPIE
3 Experience with Implementation
4 Related Work
5 Conclusion
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken