Nominal Abstraction

Details Nominal Abstraction Nominal Abstraction

2009-08-10

arxiv.org/abs/0908.1390v3

Computer Science

Logic in Computer Science

To appear in the Journal of Information and Computation

Scientific paper

Recursive relational specifications are commonly used to describe the computational structure of formal systems. Recent research in proof theory has identified two features that facilitate direct, logic-based reasoning about such descriptions: the interpretation of atomic judgments through recursive definitions and an encoding of binding constructs via generic judgments. However, logics encompassing these two features do not currently allow for the definition of relations that embody dynamic aspects related to binding, a capability needed in many reasoning tasks. We propose a new relation between terms called nominal abstraction as a means for overcoming this deficiency. We incorporate nominal abstraction into a rich logic also including definitions, generic quantification, induction, and co-induction that we then prove to be consistent. We present examples to show that this logic can provide elegant treatments of binding contexts that appear in many proofs, such as those establishing properties of typing calculi and of arbitrarily cascading substitutions that play a role in reducibility arguments.

Affiliated with

Also associated with

No associations

Rating

Nominal Abstraction does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Nominal Abstraction, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Nominal Abstraction will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-163986