Typing in reflective combinatory logic

We study Artemov’s Reflective Combinatory Logic . We provide the explicit definition of types for and prove that every well-formed term has a unique type. We establish that the typability testing and detailed type restoration can be done in polynomial time and that the derivability relation for is decidable and PSPACE-complete. These results also formalize the intended semantics of the type t:F in . Terms store the complete information about the judgment “t is a term of type F”, and this information can be extracted by the type restoration algorithm.