Fixed-Point Logic with the Approximation Modality and Its Kripke Completeness
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.
KeywordsInduction Hypothesis Modal Logic Typing System Approximation Modality Completeness Theorem
Unable to display preview. Download preview PDF.
- 1.Nakano, H.: A modality for recursion. In: Proceedings of the 15th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press (2000) 255–266Google Scholar
- 2.Nakano, H.: A modality for recursion (technical report). Available as http://www602.math.ryukoku.ac.jp/~nakano/papers/modality-tr01.ps (2001)
- 5.Boolos, G.: The logic of provability. Cambridge University Press (1993)Google Scholar
- 6.Barendregt, H.P.: Lambda calculi with types. In Abramsky, S., Gabbay, D.M., Maibaum, T.S.E.,eds.: Handbook of Logic in Computer Science. Volume 2. Oxford University Press (1992) 118–309Google Scholar