Publication details

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

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