Fixed-Point Logic with the Approximation Modality and Its Kripke Completeness

  • Hiroshi Nakano
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2215)


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.


Induction Hypothesis Modal Logic Typing System Approximation Modality Completeness Theorem 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 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. 2.
    Nakano, H.: A modality for recursion (technical report). Available as (2001)
  3. 3.
    Hindley, R.: The completeness theorem for typing λ-terms. Theoretical Computer Science 22 (1983) 1–17zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Hindley, R.: Curry’s type-rules are complete with respect to F-sematics too. Theoretical Computer Science 22 (1983) 127–133zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Boolos, G.: The logic of provability. Cambridge University Press (1993)Google Scholar
  6. 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
  7. 7.
    Cardone, F., Coppo, M.: Type inference with recursive types: syntax and semantics. Information and Computation 92 (1991) 48–80zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    Amadio, R.M., Cardelli, L.: Subtyping recursive types. ACM Transactions on Programming Languages and Systems 15 (1993) 575–631CrossRefGoogle Scholar
  9. 9.
    Courcelle, B.: Fundamental properties of infinite trees. Theoretical Computer Science 25 (1983) 95–169zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Hiroshi Nakano
    • 1
  1. 1.Ryukoku UniversityJapan

Personalised recommendations