Aarhus University Seal / Aarhus Universitets segl

A Metric Model of Lambda Calculus with Guarded Recursion

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

  • Lars Birkedal
  • Jan Swinghammer, Saarland University, Germany
  • Kristian Støvring, IT University of Copenhagen, Denmark
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
Original languageEnglish
Title of host publicationFixed Points in Computer Science 2010 : Brno, August 21-22, 2010
EditorsLuigi Santocanale
Number of pages6
Publication year2010
Publication statusPublished - 2010
Externally publishedYes

See relations at Aarhus University Citationformats

ID: 81421056