Towards Reasoning About Properties of Imperative Programs using Linear Logic

TL;DR

This paper introduces a logical framework based on linear logic, specifically Lolli, to model and reason about imperative program properties by mimicking natural semantics derivations.

Contribution

It presents a novel approach using Lolli to encode natural semantics rules, enabling reasoning about imperative programs within a logical proof system.

Findings

Lolli effectively models state and resources in imperative programs.

Proofs in Lolli correspond to natural semantics derivations.

The approach facilitates formal reasoning about program behavior.

Abstract

In this paper we propose an approach to reasoning about properties of imperative programs. We assume in this context that the meanings of program constructs are described using rules in the natural semantics style with the additional observation that these rules may involve the treatment of state. Our approach involves modeling natural semantics style rules within a logic and then reasoning about the behavior of particular programs by reasoning about proofs in that logic. A key aspect of our proposal is to use a fragment of linear logic called Lolli (invented by Hodas and Miller) to model natural semantics style descriptions. Being based on linear logic, Lolli can provide logical expression to resources such as state. Lolli additionally possesses proof-theoretic properties that allow it to encode natural semantics style descriptions in such a way that proofs in Lolli mimic the structure of derivations based on the natural semantics rules. We will discuss these properties of Lolli and demonstrate how they can be exploited in modeling the semantics of imperative programs and in reasoning about such models.