Name
Title | ||
|---|---|---|
The calculus of nominal inductive constructions: an intensional approach to encoding name-bindings |
Abstract | ||
|---|---|---|
Although name-bindings are ubiquitous in computer science, they are well-known to be cumbersome to encode and reason about in logic and type theory. There are many proposed solutions to this problem in the literature, but most of these proposals, however, have been extensional, meaning they are defined in terms of other concepts in the theory. This makes it difficult to apply these proposals in intensional theories like the Calculus of Inductive Constructions, or CIC. In this paper, we introduce an approach to encoding name-bindings that is intensional, as it attempts to capture the meaning of a name-binding in itself. This approach combines in a straightforward manner with CIC to form the Calculus of Nominal Inductive Constructions, or CNIC. CNIC supports induction over data containing bindings, comparing of names for equality, and associating meta-language types with names in a fashion similar to HOAS, features which have been shown difficult to support in practice. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1145/1577824.1577836 | LFMTP |
Keywords | Field | DocType |
meta-language type,nominal inductive construction,proposed solution,type theory,intensional approach,nominal inductive constructions,straightforward manner,inductive constructions,computer science,encoding name-bindings,intensional theory,universal algebra | ENCODE,Type theory,Extensional definition,Mathematics,Universal algebra,Calculus,Encoding (memory) | Conference |
Citations | PageRank | References |
10 | 0.54 | 13 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Edwin Westbrook | 1 | 92 | 7.24 |
| Aaron Stump | 2 | 10 | 0.54 |
| Evan Austin | 3 | 12 | 1.61 |