This volume presents the proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and Its Applications held in Valetta, Malta in September 1994.
Besides 3 invited papers, the proceedings contains 27 refereed papers selected from 42 submissions. In total the book presents many new results by leading researchers working on the design and applications of theorem provers for higher order logic. In particular, this book gives a thorough state-of-the-art report on applications of the HOL system, one of the most widely used theorem provers for higher order logic.
Author(s): Sten Agerholm (auth.), Thomas F. Melham, Juanito Camilleri (eds.)
Series: Lecture Notes in Computer Science 859
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 1994
Language: English
Pages: 477
Tags: Mathematical Logic and Formal Languages; Artificial Intelligence (incl. Robotics); Mathematical Logic and Foundations
LCF examples in HOL....Pages 1-16
A graphical tool for proving UNITY progress....Pages 17-32
Reasoning about a class of linear systems of equations in HOL....Pages 33-48
Towards a HOL theory of memory....Pages 49-64
Providing tractable security analyses in HOL....Pages 65-80
Highlighting the lambda-free fragment of Automath....Pages 81-96
First-order automation for higher-order-logic theorem proving....Pages 97-112
Symbolic animation as a proof tool....Pages 113-127
Datatypes in L2....Pages 128-143
A formal theory of undirected graphs in higher-order logc....Pages 144-157
Mechanical verification of distributed algorithms in higher-order logic....Pages 158-176
Tracking design changes with formal verification....Pages 177-192
Weak systems of set theory related to HOL....Pages 193-204
Interval-semantic component models and the efficient verification of transaction-level circuit behavior....Pages 205-220
An interpretation of Noden in HOL....Pages 221-234
Reasoning about real circuits....Pages 235-253
Binary decision diagrams as a HOL derived rule....Pages 254-268
Trustworthy tools for trustworthy programs: A verified verification condition generator....Pages 269-284
S: A machine readable specification notation based on higher order logic....Pages 285-299
An engineering approach to formal digital system design....Pages 300-315
Generating designs using an Algorithmic Register Transfer Language with formal semantics....Pages 316-331
A HOL formalisation of the Temporal Logic of Actions....Pages 332-345
Studying the ML module system in HOL....Pages 346-361
Towards a mechanically supported and compositional calculus to design distributed algorithms....Pages 362-377
Simplifying deep embedding: A formalised code generator....Pages 378-390
Automating verification by functional abstraction at the system level....Pages 391-406
A parameterized proof manager....Pages 407-423
Implementational issues for verifying RISC-pipeline conflicts in HOL....Pages 424-439
Specifying instruction-set architectures in HOL: A primer....Pages 440-455
Representing higher-order logic proofs in HOL....Pages 456-470
