Rewrite Semantics for Guarded Recursion

Abstract

Guarded recursion in the style of Nakano offers an approach to adding recursion to type theory in a consistent way. Recent work has shown that guarded recursion is useful for operational reasoning about programming languages with advanced features, and can also be used as a synthetic form of domain theory in which denotational models of programming languages with recursion can be constructed and reasoned about. We present a reduction semantics for a type theory with guarded recursive types and quantification over clocks in the style of Atkey and McBride.

Categories: Type Theory, Rewriting

Tags: Type Theory, Reduction Semantics, Strongly Normalising, Confluence, Rewriting