Combining generic judgments with recursive definitions

Many semantical aspects of programming languages are specified through calculi for constructing proofs: consider, for example, the specification of structured operational semantics, labeled transition systems, and typing systems. Recent proof theory research has identified two 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. In particular, they have not contained the ability to form definitions of 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 part of the integration allows recursive definitions to defin...

• Type: Journal
• Year: 2008
• Where: CORR
• Authors: Andrew Gacek, Dale Miller, Gopalan Nadathur
• Keywords: Atomic Judgments, CORR 2008, Education, Generic Judgments, Many Semantical Aspects