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

ABSTRACT

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.

REFERENCES

• 1: J. Cheney. A simpler proof theory for nominal logic. In V. Sassone, editor, Proc. FoSSaCS, volume 3441 of Lecture Notes in Computer Science, pages 379--394. Springer, 2005.
• 2: Marcelo Fiore , Gordon Plotkin , Daniele Turi, Abstract Syntax and Variable Binding, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p.193, July 02-05, 1999
• 3: M. J. Gabbay. Fresh logic: a logic of FM. Submitted, 2003.
• 4: Furio Honsell , Marino Miculan , Ivan Scagnetto, An Axiomatic Approach to Metareasoning on Nominal Algebras in HOAS, Proceedings of the 28th International Colloquium on Automata, Languages and Programming,, p.963-978, July 08-12, 2001
• 5: Furio Honsell , Marino Miculan , Ivan Scagnetto, &pgr;-calculus in (Co)inductive-type theory, Theoretical Computer Science, v.253 n.2, p.239-285, Feb. 28, 2001 [doi>10.1016/S0304-3975(00)00095-5]
• 6: INRIA. The Coq Proof Assistant, version 8, 2004. Available at http://coq.inria.fr/doc/main.html .
• 7: Dale Miller , Catuscia Palmidessi, Foundational aspects of syntax, ACM Computing Surveys (CSUR), v.31 n.3es, Sept. 1999 [doi>10.1145/333580.333590]
• 8: Dale Miller , Alwen Tiu, A Proof Theory for Generic Judgments: An extended abstract, Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, p.118, June 22-25, 2003
• 9: Andrew M. Pitts, Nominal logic, a first order theory of names and binding, Information and Computation, v.186 n.2, p.165-193, 01 November 2003 [doi>10.1016/S0890-5401(03)00138-X]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Syntax

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems; Mechanical theorem proving

General Terms:
Languages, Theory, Verification

Keywords:
calculus of inductive constructions, languages with binders, logical expressivity, nominal logics, theory of contexts