2017/03/29 by Hiroshi Nakano, Nakano, Hiroshi
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1703.09907
openalex publication_date 2017/03/29 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.