Rewrite Semantics for Guarded Recursion in Type Theory
Talk, FP Lunch, Functional Programming Lab, University of Nottingham, UK, 16/09/2016.
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