A modal typing system for self-referential programs and specifications

TL;DR

This paper introduces a modal typing system that manages self-referential formulas, including negative references, enabling the formal analysis of fixed-point programs and object-oriented methods within a logical framework.

Contribution

It presents a novel modal typing system that handles self-referential and negative self-referential formulas, expanding the scope of formal semantics for recursive and object-oriented programs.

Findings

Provides a basis for axiomatic semantics of self-referential programs

Enables natural construction of recursive programs in proofs-as-programs paradigm

Addresses logical contradictions in self-reference handling

Abstract

This paper proposes a modal typing system that enables us to handle self-referential formulae, including ones with negative self-references, which on one hand, would introduce a logical contradiction, namely Russell's paradox, in the conventional setting, while on the other hand, are necessary to capture a certain class of programs such as fixed-point combinators and objects with so-called binary methods in object-oriented programming. The proposed system provides a basis for axiomatic semantics of such a wider range of programs and a new framework for natural construction of recursive programs in the proofs-as-programs paradigm.