# 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.

## Key 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.

---
Source: https://tomesphere.com/paper/1703.09907