Publication details
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
@MISC{BirkedalEtAl:2010:A-Metric,
title = {A Metric Model of Lambda Calculus with Guarded Recursion},
author = {Lars Birkedal and Jan Schwinghammer and Kristian Støvring},
year = {2010},
month = {Aug},
booktitle = {Fixed Points in Computer Science (FICS'10)},
howpublished = {Informal workshop proceedings},
}
Login to edit
Legal notice, Privacy policy