Patrick Bahr IT University of Copenhagen

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