Properties of Terms in Continuation-Passing Style in an Ordered Logical Framework

A logical framework is a meta-language for the formalization of deductive systems as used in the description of logics and programming languages. It should directly support common notions and techniques of this domain, thereby achieving two related goals: on one hand, it provides a conceptual tool for the concise definition and rigorous reasoning about programming languages and logics; on the other hand, it significantly reduces the effort required to actually implement deductive systems.