Rewrite Semantics for Guarded Recursion in Type Theory

Patrick Bahr, presenting joint work with Rasmus Ejlers Møgelberg and Hans Bugge Grathwohl
Talk, FP Lunch, Functional Programming Lab, University of Nottingham, UK, 16/09/2016.


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