# Combining generic judgments with recursive definitions

## A. Gacek, D. Miller, G. Nadathur

### Proceedings of LICS 2008 (F. Pfenning, ed.), IEEE Computer Society Press, June 2008, pp. 33-44

Many semantical aspects of programming languages, such as their
operational semantics and their type assignment calculi, are specified
by describing appropriate proof systems. Recent research has
identified two proof-theoretic features that allow direct, logic-based
reasoning about such descriptions: the treatment of atomic judgments
as fixed points (recursive definitions) and an encoding of binding
constructs via generic judgments. However, the logics encompassing
these two features have thus far treated them orthogonally: that is,
they do not provide the ability to define object-logic properties that
themselves depend on an intrinsic treatment of binding. We propose a
new and simple integration of these features within an intuitionistic
logic enhanced with induction over natural numbers and we show that
the resulting logic is consistent. The pivotal benefit of the
integration is that it allows recursive definitions to not just encode
simple, traditional forms of atomic judgments but also to capture
generic properties pertaining to such judgments. The usefulness of
this logic is illustrated by showing how it can provide elegant
treatments of object-logic contexts that appear in proofs involving
typing calculi and of arbitrarily cascading substitutions that play a
role in reducibility arguments.