Higher Order Logic Theorem Proving and its Applications
Latest Publications

TOTAL DOCUMENTS

(FIVE YEARS 0)

H-INDEX

(FIVE YEARS 0)

Published By Elsevier

9780444898807

Latest Documents Most Cited Documents Contributed Authors Related Sources Related Keywords

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

Higher Order Logic Theorem Proving and its Applications ◽

10.1016/b978-0-444-89880-7.50042-5 ◽

1993 ◽

pp. 561-568 ◽

Cited By ~ 11

Author(s):

Elsa L. Gunter

Download Full-text

Linking Other Theorem Provers to HOL Using PM: Proof Manager11This research is supported in part by the Department of Defense under contract grant DOD-MDA 904-91-C-7052.

Higher Order Logic Theorem Proving and its Applications ◽

10.1016/b978-0-444-89880-7.50040-1 ◽

1993 ◽

pp. 539-548

Author(s):

Myla Archer ◽

George Fink ◽

Lie Yang

Keyword(s):

Department Of Defense ◽

Theorem Provers

Download Full-text

Simulating Microprocessors from Formal Specifications11This research was supported in part by NSF under Research Initiation Grant MIP-9109618.

Higher Order Logic Theorem Proving and its Applications ◽

10.1016/b978-0-444-89880-7.50038-3 ◽

1993 ◽

pp. 507-525

Author(s):

Kelly M. Hall ◽

Phillip J. Windley

Download Full-text

A HOL Mechanization of The Axiomatic Semantics of a Simple Distributed Programming Language11The research reported here was funded in part by contract DOD-MDA 904-91-C-7053 with the National Security Agency's University Program.

Higher Order Logic Theorem Proving and its Applications ◽

10.1016/b978-0-444-89880-7.50028-0 ◽

1993 ◽

pp. 347-356

Author(s):

William L. Harrison ◽

Myla M. Archer ◽

Karl N. Levitt

Keyword(s):

National Security ◽

Distributed Programming ◽

Axiomatic Semantics

Download Full-text

Mechanising some Advanced Refinement Concepts

Higher Order Logic Theorem Proving and its Applications ◽

10.1016/b978-0-444-89880-7.50026-7 ◽

1993 ◽

pp. 307-326 ◽

Cited By ~ 2

Author(s):

J. von Wright ◽

J. Hekanaho ◽

P. Luostarinen ◽

T. Långbacka

Download Full-text

Introducing well-founded function definitions in HOL

Higher Order Logic Theorem Proving and its Applications ◽

10.1016/b978-0-444-89880-7.50014-0 ◽

1993 ◽

pp. 117-131 ◽

Cited By ~ 5

Author(s):

Mark van der Voort

Download Full-text

Efficient Representation and Computation of Tableaux Proofs

Higher Order Logic Theorem Proving and its Applications ◽

10.1016/b978-0-444-89880-7.50009-7 ◽

1993 ◽

pp. 39-57

Author(s):

Klaus Schneider ◽

Ramayya Kumar ◽

Thomas Kropf

Keyword(s):

Efficient Representation

Download Full-text

Adding New Rules to an LCF-style Logic Implementation

Higher Order Logic Theorem Proving and its Applications ◽

10.1016/b978-0-444-89880-7.50041-3 ◽

1993 ◽

pp. 549-559 ◽

Cited By ~ 1

Author(s):

Konrad Slind

Download Full-text

Specification and formal synthesis of digital circuits

Higher Order Logic Theorem Proving and its Applications ◽

10.1016/b978-0-444-89880-7.50036-x ◽

1993 ◽

pp. 475-484 ◽

Cited By ~ 1

Author(s):

M. Bombana ◽

P. Cavalloro ◽

G. Zaza

Keyword(s):

Digital Circuits ◽

Formal Synthesis

Download Full-text

Deriving a Correct Computer

Higher Order Logic Theorem Proving and its Applications ◽

10.1016/b978-0-444-89880-7.50034-6 ◽

1993 ◽

pp. 449-458 ◽

Cited By ~ 2

Author(s):

Li-Guo Wang

Download Full-text

Higher Order Logic Theorem Proving and its ApplicationsLatest Publications

TOTAL DOCUMENTS

H-INDEX

Published By Elsevier

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

Linking Other Theorem Provers to HOL Using PM: Proof Manager11This research is supported in part by the Department of Defense under contract grant DOD-MDA 904-91-C-7052.

Simulating Microprocessors from Formal Specifications11This research was supported in part by NSF under Research Initiation Grant MIP-9109618.

A HOL Mechanization of The Axiomatic Semantics of a Simple Distributed Programming Language11The research reported here was funded in part by contract DOD-MDA 904-91-C-7053 with the National Security Agency's University Program.

Mechanising some Advanced Refinement Concepts

Introducing well-founded function definitions in HOL

Efficient Representation and Computation of Tableaux Proofs

Adding New Rules to an LCF-style Logic Implementation

Specification and formal synthesis of digital circuits

Deriving a Correct Computer

Higher Order Logic Theorem Proving and its Applications
Latest Publications