The Community for Technology Leaders
1991 International Workshop on the HOL Theorem Proving System and Its Applications (1991)
Davis, CA, USA
Aug. 28, 1991 to Aug. 30, 1991
ISBN: 0-8186-2460-4
TABLE OF CONTENTS

Introduction To The Hol System (PDF)

M. Gordon , New Museums Site
pp. 2-3

HOL Around The World (PDF)

S. Kalvala , University of California at Davis
pp. 4-12

Verification Of Integrated Subsystems (PDF)

E.T. Schubert , University of California
pp. 38-51

Reasoning About Software (PDF)

R. Hale , SRI International
pp. 52-58

Mechanizing Security In HOL (PDF)

W.L. Harrison , University of California
pp. 63-66

Learning To Use HOL (PDF)

P. Loewenstein , Mitsubishi Electronics America Inc.
pp. 67-74

Mechanizing The Temporal Logic Of Actions In HOL (PDF)

J. von Wright , Abo Akademi University
pp. 155-159

Window Inference In The HOL System (PDF)

J. Grundy , University of Cambridge
pp. 177-189

Mechanizing Program Verification in HOL (PDF)

S. Agerholm , Aarhus University
pp. 208-222

Proof Of Program Transformations (PDF)

R. Roxas , The Australian National University
pp. 223-230

A Report On ICL HOL (PDF)

R.D. Arthan , ICL Secure Systems
pp. 280-283

PM: A Proof Manager For HOL And Other Provers (PDF)

G. Fink , University of California at Davis
pp. 286-304

Developing An Interface For HOL (PDF)

S. Kalvala , University of California at Davis
pp. 305-317

A Package For Inductive Relation Definitions In HOL (PDF)

T.F. Melham , University of Cambridge Computer Laboratory
pp. 350-357

Recursive Boolean Functions In HOL (PDF)

F. Andersen , TFL - Telecommunications Research Laboratory
pp. 367-377

Proof Based Computation (PDF)

M.C. Newey , The Australian National University
pp. 380-383

Reasoning About Petri Nets In HOL (PDF)

E. de Barros Lucena , University of Cambridge Computer Laboratory
pp. 384-394

Author index (PDF)

pp. 411
90 ms
(Ver 3.3 (11022016))