Typing in reflective combinatory logic

We study Artemov’s Reflective Combinatory Logic RCL → . We provide the explicit definition of types for RCL → 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 RCL → is decidable and PSPACE-complete. These results also formalize the intended semantics of the type t : F in RCL → . Terms RCL → 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.