Name
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. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1145/1088454.1088460 | MERLIN |
Keywords | DocType | ISBN |
strict extension,nominal logic,sequent proof system,natural-deduction style proof system,j. cheney,weak hoas encoding,intuitionistic nominal logic,translating specification,natural deduction | Conference | 1-59593-072-8 |
Citations | PageRank | References |
9 | 0.51 | 7 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Marino Miculan | 1 | 502 | 43.24 |
| Ivan Scagnetto | 2 | 232 | 20.87 |
| Furio Honsell | 3 | 1254 | 146.59 |