Higher Order Logic Theorem Proving and Its Applications: 6th International Workshop, HUG '93, Vancouver, B.C., Canada, August 11-13, 1993. ProceedingsJeffrey J. Joyce, Carl-Johan H. Seger Springer Science & Business Media, 28/04/1994 - 526 من الصفحات This volume constitutes the refereed proceedings of the 1993 Higher-Order Logic User's Group Workshop, held at the University of British Columbia in August 1993. The workshop was sponsored by the Centre for Integrated Computer System Research. It was the sixth in the series of annual international workshops dedicated to the topic of Higher-Order Logic theorem proving, its usage in the HOL system, and its applications. The volume contains 40 papers, including an invited paper by David Parnas, McMaster University, Canada, entitled "Some theorems we should prove". |
المحتوى
Program Verification using HOLUNITY | xi |
Graph model of LAMBDA in Higher Order Logic | 14 |
Mechanizing a Programming Logic for the Concurrent Programming Language microSR in HOL | 27 |
Reasoning with the Formal Definition of Standard ML in HOL | 41 |
HOLML | 59 |
Structure and Behaviour in Hardware Verification | 73 |
Degrees of Formality in Shallow Embedding Hardware Description Languages in HOL | 87 |
A Functional Approach for Formalizing Regular Hardware Structures | 99 |
Implementing a Methodology for Formally Verifying RISC Processors in HOL | 279 |
Domain Theory in HOL | 293 |
Predicates Temporal Logic and Simulations | 308 |
Formalization of Variables Access Constraints to Support Compositionality of Liveness Properties | 322 |
The Semantics of Statecharts in HOL | 336 |
ValuePassing CCS in HOL | 350 |
An Interactive and Automatic Tool for Proving Theorems of Type Theory | 364 |
the word Library | 369 |
A Proof Development System for the HOL | 113 |
A HOL Package for Reasoning about Relations Defined by Mutual Induction | 127 |
A Broader Class of Trees for Recursive Type Definitions for HOL | 139 |
Some Theorems We Should Prove | 153 |
Using PVS to Prove Some Theorems of David Parnas | 161 |
Extending the HOL Theorem Prover with a Computer Algebra System to Reason About the Reals | 172 |
ModelChecking inside a GeneralPurpose TheoremProver | 183 |
Linking Higher Order Logic to a VLSI CAD System | 197 |
Alternative Proof Procedures for FiniteState Machines in HigherOrder Logic | 211 |
A Formalization of Abstraction in LAMBDA | 225 |
Report on the UCD Microcoded Viper Verification Project | 237 |
Verification of the Tamarack3 Microprocessor in A Hybrid Verification Environment | 251 |
Abstraction Techniques for Modeling RealWorld Interface Chips | 265 |
Eliminating HigherOrder Quantifiers to Obtain Decision Procedures for Hardware Verification | 383 |
Toward a Super Duper Hardware Tactic | 397 |
A Mechanisation of Namecarrying Syntax up to AlphaConversion | 411 |
| 424 | |
AC Unification in HOL90 | 435 |
ServerProcess Restrictiveness in HOL | 448 |
A Behavioural Analysis | 462 |
On the Style of Mechanical Proving | 473 |
A Case Study in Formal Specification and Verification at Differing Levels of Abstraction using Theorem Proving and Symbolic Simulation | 487 |
Verification in Higher Order Logic of Mutual Exclusion Algorithm | 499 |
Using Isabelle to Prove Simple Theorems | 512 |
Author Index | 516 |
طبعات أخرى - عرض جميع المقتطفات
عبارات ومصطلحات مألوفة
abstraction algorithm applied approach assertions automated automatically behaviour bool boolean buffered circuits Computer Science construction constructors corresponding defined definition denotes derived described domain embedding equations evaluation example expressions finite formal formal verification formulae FSM-goals function given goal hardware description languages hardware verification Higher Order Logic higher-order logic Hoare logic HOL theorem prover implementation induction inference rules input instantiation instruction interpreter invocval pname label LAMBDA lemma lift Melham microprocessor microSR natural numbers Nuprl operation operational semantics output paper predicate proof system properties prove pure CCS PWORDLEN quantified recursive type relation represented reset result rewriting satisfies semantics signals Silage simulation specification stack Standard ML step structural subgoals subset subtrees syntax tactic Technical Report temporal theorem prover theory tion transition translation University University of Cambridge value-passing variables Viper