Conference proceeding
The calculus of nominal inductive constructions: an intensional approach to encoding name-bindings
Proceedings of the Fourth International Workshop on logical frameworks and meta-languages, pp.74-83
LFMTP '09
08/02/2009
DOI: 10.1145/1577824.1577836
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.
Details
- Title: Subtitle
- The calculus of nominal inductive constructions: an intensional approach to encoding name-bindings
- Creators
- Edwin Westbrook - Rice UniversityAaron Stump - University of IowaEvan Austin - University of Kansas
- Resource Type
- Conference proceeding
- Publication Details
- Proceedings of the Fourth International Workshop on logical frameworks and meta-languages, pp.74-83
- Series
- LFMTP '09
- DOI
- 10.1145/1577824.1577836
- Publisher
- ACM
- Grant note
- DOI: 10.13039/100000143, name: Division of Computing and Communication Foundations, award: CSR/EHS 0720857CCF 0841554; DOI: 10.13039/100000144, name: Division of Computer and Network Systems, award: CSR/EHS 0720857CCF 0841554
- Language
- English
- Date published
- 08/02/2009
- Academic Unit
- Computer Science
- Record Identifier
- 9984259429802771
Metrics
15 Record Views