Sciweavers

CORR
2008
Springer

Combining generic judgments with recursive definitions

13 years 3 months ago
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...
Andrew Gacek, Dale Miller, Gopalan Nadathur
Added 09 Dec 2010
Updated 09 Dec 2010
Type Journal
Year 2008
Where CORR
Authors Andrew Gacek, Dale Miller, Gopalan Nadathur
Comments (0)