Sciweavers

Share
TACS
2001
Springer

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

9 years 11 months ago
Fixed-Point Logic with the Approximation Modality and Its Kripke Completeness
Abstract. 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 speciļ¬cations. 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.
Hiroshi Nakano
Added 30 Jul 2010
Updated 30 Jul 2010
Type Conference
Year 2001
Where TACS
Authors Hiroshi Nakano
Comments (0)
books