Publication details

Saarland University Computer Science

A Metric Model of Lambda Calculus with Guarded Recursion

Lars Birkedal, Jan Schwinghammer, Kristian StÝvring

Fixed Points in Computer Science (FICS'10), August 2010

We give a model for Nakano's typed lambda calculus with guarded recursive definitions in a category of metric spaces. By proving a computational adequacy result that relates the interpretation with the operational semantics, we show that the model can be used to reason about contextual equivalence.

Download PDF        Show BibTeX               


Login to edit


Webmaster, Wed Sep 16 10:47:00 2009