A Modality for Recursion? (Technical Report)

Abstract. We propose a modal logic that enables us to handle self-referential formulae, including ones withnegative 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 suchas fixed point combinators and objects with so-called binary methods in object-oriented programming. Our logic provides a basis for axiomatic semantics of such a wider range of programs and a new framework for naturalconstruction of recursive programs in the proofs-as-programs paradigm. We give the logic as a modal typing system with recursive types for the purpose of presentation, and show its soundness with respect to a realizabilityinterpretation which implies the convergence of well-typed programs according to their types