Hoare's Logic in the LF

I. Mason

Abstract: In this paper we describe several attempts at defining a simple version of Hoare's logic in the LF. This is used as a framework for discussing certain issues that are raised. We give, in detail, three different attempts at formulating Hoare's logic in the LF, only two of these are in any sense successful. Both successful versions suggest certain desiderata concerning the nature of tacticals in the LF and how they can be used in faithfully presenting logics. We also mention some alternative solutions in passing.

LFCS report ECS-LFCS-87-32

Previous | Index | Next