HOL Light is a new version of the HOL theorem prover. While retaining the reliability and
programmability of earlier versions, it is more elegant, lightweight, powerful and automatic; it …

Computer-Aided Reasoning: ACL2 Case Studies illustrates how the computer-aided
reasoning system ACL2 can be used in productive and innovative ways to design, build, and …

Abstract Development of formal proofs of correctness of programs can increase actual and
perceived reliability and facilitate better understanding of program specifications and their …

This book discusses the use of the real numbers in theorem proving. Typ ically, theorem
provers only support a few'discrete'datatypes such as the natural numbers. However the …

A domain-specific language can be implemented by embedding within a general-purpose
host language. This embedding may be deep or shallow, depending on whether terms in the …

By interactive theorem proving, we mean some arrangement where the machine and a
human user work together interactively to produce a formal proof. There is a wide spectrum …

We have previously proposed SecureUML, an expressive UML-based language for
constructing security-design models, which are models that combine design specifications …

This article presents a Hoare‐style calculus for a substantial subset of Java Card, which we
call Java ^ℓight. In particular, the language includes side‐effecting expressions, mutual …

Dr. Melham shows here how formal logic can be used to specify the behavior of hardware
designs and reason about their correctness. A primary theme of the book is the use of …

It is well-known that the simply typed lambda-calculus is modeled by any cartesian closed
category (CCC). This correspondence suggests giving typed functional programs a variety of …