Higher Order Logic Theorem Proving and its Applications - Proceedings of the IFIP TC10/WG10.2 International Workshop on Higher Order Logic Theorem Proving and its Applications - HOL '92 Leuven, Belgium, 21-24 September 1992

Front Cover

Higher Order Logic Theorem Proving and its Applications

Copyright Page

Table of Contents

Preface

Conference organization

Part 1. Mathematical Logic

Chapter 1. The HOL Logic Extended with Quantification overType Variables

Abstract

1 Introduction

2 Types and polymorphism in HOL

3 Motivation

4 Universal quantification over types

5 Existential quantification over types

6 Implementation

Acknowledgements

References

Chapter 2. A Lazy Approach to Fully-Expansive TheoremProving

Abstract

1 Introduction

2 A Simple Form of Lazy Theorem

3 Lazy Conversions

4 Lazy Theorems as an Abstract Type

5 Lazy Inference Rules

6 Three Modes of Operation

7 Results

8 A Complete Lazy System

9 Applications

10 Conclusions and Future Work

Acknowledgements

References

Chapter 3. Efficient Representation and Computation of Tableaux Proofs

Abstract

1 Introduction

2 The Tableau Graph Calculus CTG

3 Algorithmic aspects

4 Implement at ional details concerning extensions

5 Embedding CTG in HOL

6 Summary

References

Chapter 4. A Note on Interactive Theorem Proving with Theorem Continuation Functions

Abstract

1 An Example

2 The Technique

3 Another Example

Appendix: The Code

Acknowledgements

References

Chapter 5. A Sequent Formulation of a Logic of Predicates in HOL

Abstract

1 A Logic of Predicates

2 Applications of LP

3 Lifting Tactics and Theorem Tactics

4 Outline of Implementation

Acknowledgements

References

Chapter 6. A Classical Type Theory with Transfinite Types

Abstract

1 Introduction

2 The Metalanguage

3 Terms, Assertions, Environments, and Sequents

4 Set Theoretic Closure Conditions

5 Structures, Models, Denotation, Satisfaction, Validity, and Consequence

6 Abbreviations

7 Inferences, Rules of Inference, Derivations, and Derivability

8 The Monotonicity Rule

9 Closure Rules

10 Conversion Rules

11 Assignment Rules

12 Morphologies

13 Boolean Rules

14 Bases, Theoremhood, and Consistency

15 Concluding Remarks

References

Part 2: Induction

Chapter 7. Unification-Based Induction

Abstract

1 Introduction

2 The Proof System LAMBDA

3 Weil-Founded Induction in LAMBDA

4 Finding an Induction Approach

5 The Completion of Induction Proofs

6 Additional Problems

7 Conclusions

References

Chapter 8. Introducing well-founded function definitions in HOL

Abstract

1 Introduction

2 Concepts and definitions

3 The introduction scheme

4 Examples

5 Formalisation

6 Examples continued

7 Conclusions

References

Chapter 9. Boyer-Moore Automation for the HOL System

Abstract

1 Introduction

2 Comparison between the Boyer-Moore Prover and the HOL Implementation

3 System-Wide Features

4 The Heuristics

5 The Automatic Prover in Use

6 Results

7 Remarks

References

Part 3: General Modelling and Proofs

Chapter 10. Constructing the real numbers in HOL

Abstract

1 Constructing the real numbers

2 Building on the real number axioms

3 Applications

4 Conclusion and related work

5 Acknowledgements

References

Chapter 11. Modelling Generic Hardware Structures by Abstract Datatypes

Abstract

1 Introduction

2 The Abstract Datatype

3 Using the ADT

4 Summary and future work

References

Chapter 12. A Methodology for Reusable Hardware Proofs

Abstract

1 Introduction

2 Background

3 Hardware Verification with Dependent Types

4 Examples

Acknowledgements

References

Chapter 13. Abstract Theories in HOL

Abstract

1 Introduction

2 Abstract Theories

3 Using the Abstract Theory Package

4 Example: Group Theory

5 Conclusions

References

Chapter 14. Machine Abstraction in Microprocessor Specification

Abstract

1 Introduction

2 A Separation of Concerns

3 Machine Abstraction

4 An Example of Machine Abstraction

5 Advantages

6 Disadvantages

7 Application Areas

8 Conclusions

9 Acknowledgements

References

Part 4: Formalizing and Modelling ofAutomata

Chapter 15. A Formal Theory of Simulations Between Infinite Automata

Abstract

1 Introduction

2 The HOL logic

3 The Automaton Model

4 Simulations between Automata

5 Safety Properties

6 Automata and Safety Properties

7 Constructions on Automata

8 Extending the use of Simulation

9 Examples

10 Conclusion

References

Chapter 16. A Comparison between Statecharts and State Transition Assertions

Abstract

1 Introduction

2 Terminology

3 Statecharts

4 State Transition Assertions

5 An Example

6 Differences Between STAs and Statecharts

7 Issues for Connecting Real-time Specification and Verification Techniques

8 Future Work

9 Summary

10 Acknowledgements

References

Chapter 17. An Embedding of Timed Transition Systems in HOL

Abstract

1 Introduction

2 Example: A Traffic Light Controller

3 Real-Time Temporal Logic

4 Timed Transition Systems

5 Timed Transition Diagrams

6 Verification

References

Chapter 18. Formalizing a Modal Logic for CCS in the HOL Theorem Prover

Abstract

1 Introduction

2 CCS

3 Mechanization of CCS in HOL

4 Proving Modal Properties of CCS Processes in HOL

5 Related Work and Conclusions

Acknowledgements

References

Chapter 19. Modelling Non-Deterministic Systems in HOL

Abstract

1 Introduction

2 System Model

3 Non—Deterministic Ordering

4 Non—Deterministic Outputs

5 Conclusion

References

Part 5: Program Verification

Chapter 20. Mechanising some Advanced Refinement Concepts

Abstract

1 Introduction

2 The refinement calculus

3 The refinement calculus as a theory of HOL

4 Data refining loops in HOL

5 Backwards data refinement

6 Superposition refinement

7 Conclusion

References

Chapter 21. Deriving Correctness Properties of Compiled Code

Abstract

1. Introduction

2. Vista

3· The Relational Semantics of Vista

4. A Derived Programming Logic for Vista

5. A Verified Compiler

6. Deriving Correctness Theorems about Object Code

7. Related Work

8. Conclusions

Acknowledgements

References

Chapter 22. A HOL Mechanization of The Axiomatic Semantics of a Simple Distributed Programming Language¹

1 Introduction

2 Motivation

3 Axiomatic Semantics Of Message Passing

4 Our Target Distributed Language

5 The HOL Mechanization of the Semantics

6 Discussion

References

Part 6: Hardware Description LanguageSemantics

Chapter 23. A Formalisation of the VHDL Simulation Cycle

Abstract

1 Introduction

2 Overview of VHDL

3 Related Work

4 Philosophy

5 Intuition behind the Semantics

6 The Femto-VHDL Subset

7 The Semantic Framework

8 The Semantics of Femto-VHDL

9 Femto-VHDL in HOL

10 Conclusions and Future Work

11 Acknowledgements

References

Chapter 24. The Formal Semantics Definition of a Multi-Rate DSPSpecification Language in HOL ¹

Abstract

1 Introduction

2 An informal description of Silage

3 Previous work and extensions

4 HOL definitions and functions described in ML

5 Denotational semantics of expressions

6 Denotational Semantics of Definitions

7 The Denotational Semantics of Silage Functions

8 Reasoning about Silage Programs

9 Status of the work

10 Conclusions

11 Acknowledgements

References

Chapter 25. Design-Flow Graph Partitioning

Abstract

1 Introduction

2 Scheduling of Flow-Graphs

3 Graph Restructuring

4 Future Higher-Order Operations

5 Acknowledgements

References

Part 7: Hardware Verification Methodologies

Chapter 26. Implementation and Use of Annotations in HOL

Abstract

1 Introduction

2 Related work

3 Proposed approach

4 Basic structures

5 Uses of annotations

6 Conclusions and further work

Acknowledgements

References

Chapter 27. Towards a Formal Verification of a Floating Point Coprocessor and its Composition with a Central Processing Unit ¹

Abstract

1 Introduction

2 Verifying the composition of verified systems

3 The floating-point coprocessor architecture

4 Verifying the FPC top-level from three communicatingunits

5 Verifying the concurrent top level

6 Verifying the sequential top level

7 Discussion

References

Chapter 28. Deriving a Correct Computer

Abstract

1 Introduction

2 Specification

3 Axioms

4 Derivation

5 Implementation

6 Conclusion and Further Work

References

Chapter 29. Formal Tools for Tri-State Design in Busses

Abstract

1 Introduction

2 The LAMBDA System

3 Industrial Example

4 Conclusions

5 Acknowledgements

References

Chapter 30. Specification and formal synthesis of digital circuits

Abstract

1. INTRODUCTION

2. POST DESIGN VALIDATION WITH OTTER

3. FORMALLY BASED SYNTHESIS WITH LAMBDA/DIALOG

4. INTRODUCTION OF FORMAL TOOLS INTO A DESIGN FLOW

5. CONCLUSIONS

6. REFERENCES

Part 8: Simulation in Higher Order Logic

Chapter 31. Operational Semantics Based Formal Symbolic Simulation

Abstract

1 Introduction

2 picoELLA

3 A picoELLA Semantics and Its Embedding in Higher Order Logic

4 Examples

5 Conclusions

References

Chapter 32. Simulating Microprocessors from Formal Specifications

Abstract

1 Introduction

2 The Generic Interpreter Theory

3 Generic Interpreter Theory Simulator

4 Tamarack—3 Example

5 Conclusion

References

Chapter 33. Executing HOL Specifications: Towards an Evaluation Semantics for Classical Higher Order Logic

Abstract

1 Introduction

2 Issues in Evaluating Specifications

3 Translation Overview

4 Example Translation: Step b y Step

5 Limitations

6 Towards Evaluation Semantics

7 Summary and Future Work

Acknowledgements

References

Appendix: Example Evaluation Sessions

Part 9: Extended uses of Higher Order Logic

Chapter 34. Linking Other Theorem Provers to HOL Using PM: Proof Manager¹

Abstract

1.Introduction

2. Improvements to PM as a proof manager

3. Translation from HOL to other theorem provers

4. Using PM with multiple provers

5. An example of using multiple provers with PM

6. References

Chapter 35. Adding New Rules to an LCF-style Logic Implementation

Abstract

1 Introduction

2 The formalization of programs

3 First class environments

4 Program equivalence

5 Adding a new rule

6 Methodology, or Modelling the Growth of an Implementation

7 Related Work

8 Conclusions and Future Work

9 Acknowledgements

References

Chapter 36. Why We Can't have SML Style datatype Declarations in HOL

Abstract

1 Introduction

2 Differences Between SML Types and HOL Types

3 The HOL Proof that the Function Space Can't Be Embedded

4 Constraints on type constructors that don't work

5 What we can build

References