Translating specifications from nominal logic to CIC with the 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, inspired by a sequent proof system recently proposed by J. Cheney. We present a translation of terms, formulas and judgments of NINL, into terms and propositions of CIC, via a weak HOAS encoding. It turns out that the (translation of the) axioms and rules of NINL are derivable in CIC extended with the Theory of Contexts (CIC/ToC), and that in the latter we can prove also sequents which are not derivable in NINL. Thus, CIC/ToC can be seen as a strict extension of NINL. Categories and Subject Descriptors D.3.1 [Formal Definitions and Theory]: Syntax; F.3.1 [Specifying and Reasoning about Programs]: Specification techniques; F.4.1 [Mathematical Logic]: Lambda calculus and related systems; Mechanical theorem proving General Terms Theory, Languages, ...

• Type: Conference
• Year: 2005
• Where: ICFP
• Authors: Marino Miculan, Ivan Scagnetto, Furio Honsell
• Keywords: General Terms Theory, ICFP 2005, Intuitionistic Nominal Logic, Nominal Logics, Programming Languages