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

Legal notice, Privacy policy