A metric model of lambda calculus with guarded recursion

Lars Birkedal; Jan Schwinghammer; Kristian Støvring

A metric model of lambda calculus with guarded recursion

Lars Birkedal, Jan Schwinghammer, Kristian Støvring

Department of Computer Science

Abstract

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 language	English
Title of host publication	7th Workshop on Fixed Points in Computer Science : FICS 2010
Editors	Luigi Santocanale
Number of pages	7
Publication date	2010
Pages	19-25
Publication status	Published - 2010
Event	7th Workshop on Fixed Points in Computer Science - Brno, Czech Republic Duration: 21 Aug 2010 → 22 Aug 2010 Conference number: 7

Conference

Conference	7th Workshop on Fixed Points in Computer Science
Number	7
Country/Territory	Czech Republic
City	Brno
Period	21/08/2010 → 22/08/2010

Access to Document

https://hal.archives-ouvertes.fr/hal-00512377

Cite this

@inproceedings{35778c09e087468b8b5530c8b532d31c,

title = "A metric model of lambda calculus with guarded recursion",

abstract = "We give a model for Nakano{\textquoteright}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.",

author = "Lars Birkedal and Jan Schwinghammer and Kristian St{\o}vring",

year = "2010",

language = "English",

pages = "19--25",

editor = "Luigi Santocanale",

booktitle = "7th Workshop on Fixed Points in Computer Science",

note = "7th Workshop on Fixed Points in Computer Science ; Conference date: 21-08-2010 Through 22-08-2010",

}

TY - GEN

T1 - A metric model of lambda calculus with guarded recursion

AU - Birkedal, Lars

AU - Schwinghammer, Jan

AU - Støvring, Kristian

N1 - Conference code: 7

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

M3 - Article in proceedings

SP - 19

EP - 25

BT - 7th Workshop on Fixed Points in Computer Science

A2 - Santocanale, Luigi

T2 - 7th Workshop on Fixed Points in Computer Science

Y2 - 21 August 2010 through 22 August 2010

ER -