Sciweavers

Share
ICFP
2005
ACM

Translating specifications from nominal logic to CIC with the theory of contexts

10 years 11 months ago
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, ...
Marino Miculan, Ivan Scagnetto, Furio Honsell
Related Content
Added 13 Dec 2009
Updated 13 Dec 2009
Type Conference
Year 2005
Where ICFP
Authors Marino Miculan, Ivan Scagnetto, Furio Honsell
Comments (0)
books