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

Datalogisk Institut

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.

Originalsprog	Engelsk
Titel	7th Workshop on Fixed Points in Computer Science : FICS 2010
Redaktører	Luigi Santocanale
Antal sider	7
Publikationsdato	2010
Sider	19-25
Status	Udgivet - 2010
Begivenhed	7th Workshop on Fixed Points in Computer Science - Brno, Tjekkiet Varighed: 21 aug. 2010 → 22 aug. 2010 Konferencens nummer: 7

Konference

Konference	7th Workshop on Fixed Points in Computer Science
Nummer	7
Land/Område	Tjekkiet
By	Brno
Periode	21/08/2010 → 22/08/2010

Adgang til dokumentet

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

Citationsformater

@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 -