Calculus of Inductive Constructions; Languages with binders; Logical expressivity; Nominal Logics; Theory of Contexts

We study the relation between Nominal Logic and the Theory of Contexts, two approaches for specifying and reasoning about datatypes with binders. We consider a natural-deduction style proof system for intuitionistic nominal logic, called NINL, …