We present two modal typing systems with the approximation modality, which has been proposed by the author to capture selfreferences involved in computer programs and their specifications. The systems are based on the simple and the F-semantics of types, respectively, and correspond to the same modal logic, which is considered the intuitionistic version of the logic of provability. We also show Kripke completeness of the modal logic and its decidability, which implies the decidability of type inhabitance in the typing systems.
CITATION STYLE
Nakano, H. (2001). Fixed-point logic with the approximation modality and its Kripke completeness. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2215, pp. 165–182). Springer Verlag. https://doi.org/10.1007/3-540-45500-0_8
Mendeley helps you to discover research relevant for your work.