The calculus of nominal inductive constructions
Edwin M. Westbrook, Aaron Stump, Evan Austin · 2009
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.