Combining generic judgments with recursive definitions

Andrew Gacek, Dale Miller, Gopalan Nadathur

Research output: Chapter in Book/Report/Conference proceedingConference contribution

37 Scopus citations

Abstract

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 logicenhanced 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 objectlogic contexts that appear in proofs involving typing calculi and of arbitrarily cascading substitutions that play a role in reducibility arguments.

Original languageEnglish (US)
Title of host publicationProceedings - 23rd Annual IEEE Symposium on Logic in Computer Science, LICS 2008
Pages33-44
Number of pages12
DOIs
StatePublished - 2008
Event23rd Annual IEEE Symposium on Logic in Computer Science, LICS 2008 - Pittsburgh, PA, United States
Duration: Jun 24 2008Jun 27 2008

Publication series

NameProceedings - Symposium on Logic in Computer Science
ISSN (Print)1043-6871

Other

Other23rd Annual IEEE Symposium on Logic in Computer Science, LICS 2008
Country/TerritoryUnited States
CityPittsburgh, PA
Period6/24/086/27/08

Keywords

  • Generic judgments
  • Higher-order abstract syntax
  • Proof search
  • Reasoning about operational semantics

Fingerprint

Dive into the research topics of 'Combining generic judgments with recursive definitions'. Together they form a unique fingerprint.

Cite this