Translating Specifications from Nominal Logic to CIC with the Theory of Contexts

MERLIN 2005

数学;计算机科学

Marino Miculan ; Ivan Scagnetto ; Furio Honsell

Others  :  http://homepages.inf.ed.ac.uk/rpollack/TYPES/MERLIN_05/p41-miculan.pdf
PID  :  52666

学科分类：计算机科学（综合）

来源: CEUR

【 摘 要 】

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 Pro- grams]: Specification techniques; F.4.1 [Mathematical Logic]: Lambda calculus and related systems; Mechanical theorem proving General Terms Theory, Languages, Verification.