Axiomatics for Data Refinement in Call by Value Programming Languages

J Power; M Tanaka

doi:10.1016/j.entcs.2008.12.081

Axiomatics for Data Refinement in Call by Value Programming Languages

J Power, M Tanaka

Department of Computer Science

National Institute of Information and Communications Technology

Research output: Contribution to journal › Article › peer-review

175 Downloads (Pure)

Abstract

We give a systematic category theoretic axiomatics for modelling data refinement in call by value programming languages. Our leading examples of call by value languages are extensions of the computational λ-calculus, such as FPC and languages for modelling nondeterminism, and extensions of the first order fragment of the computational λ-calculus, such as a CPS language. We give a category theoretic account of the basic setting, then show how to model contexts, then arbitrary type and term constructors, then signatures, and finally data refinement. This extends and clarifies Kinoshita and Power's work on lax logical relations for call by value languages.

Original language	English
Pages (from-to)	281-302
Number of pages	22
Journal	Electronic Notes in Theoretical Computer Science
Volume	225
DOIs	https://doi.org/10.1016/j.entcs.2008.12.081
Publication status	Published - 2 Jan 2009

Access to Document

10.1016/j.entcs.2008.12.081Licence: CC BY-NC-ND

Power_ENTCS_2009_225_281.pdf
NOTICE: this is the author’s version of a work that was accepted for publication in Electronic Notes in Theoretical Computer Science. Changes resulting from the publishing process, such as peer review, editing, corrections, structural formatting, and other quality control mechanisms may not be reflected in this document. Changes may have been made to this work since it was submitted for publication. A definitive version was subsequently published in Electronic Notes in Theoretical Computer Science, 225, 2009, DOI 10.1016/j.entcs.2008.12.081
Accepted author manuscript, 1.68 MB

Cite this

@article{f13fa3ff22d342619355509ea93ff911,

title = "Axiomatics for Data Refinement in Call by Value Programming Languages",

abstract = "We give a systematic category theoretic axiomatics for modelling data refinement in call by value programming languages. Our leading examples of call by value languages are extensions of the computational λ-calculus, such as FPC and languages for modelling nondeterminism, and extensions of the first order fragment of the computational λ-calculus, such as a CPS language. We give a category theoretic account of the basic setting, then show how to model contexts, then arbitrary type and term constructors, then signatures, and finally data refinement. This extends and clarifies Kinoshita and Power's work on lax logical relations for call by value languages.",

author = "J Power and M Tanaka",

year = "2009",

month = jan,

day = "2",

doi = "10.1016/j.entcs.2008.12.081",

language = "English",

volume = "225",

pages = "281--302",

journal = "Electronic Notes in Theoretical Computer Science",

publisher = "Elsevier B.V.",

}

TY - JOUR

T1 - Axiomatics for Data Refinement in Call by Value Programming Languages

AU - Power, J

AU - Tanaka, M

PY - 2009/1/2

Y1 - 2009/1/2

N2 - We give a systematic category theoretic axiomatics for modelling data refinement in call by value programming languages. Our leading examples of call by value languages are extensions of the computational λ-calculus, such as FPC and languages for modelling nondeterminism, and extensions of the first order fragment of the computational λ-calculus, such as a CPS language. We give a category theoretic account of the basic setting, then show how to model contexts, then arbitrary type and term constructors, then signatures, and finally data refinement. This extends and clarifies Kinoshita and Power's work on lax logical relations for call by value languages.

AB - We give a systematic category theoretic axiomatics for modelling data refinement in call by value programming languages. Our leading examples of call by value languages are extensions of the computational λ-calculus, such as FPC and languages for modelling nondeterminism, and extensions of the first order fragment of the computational λ-calculus, such as a CPS language. We give a category theoretic account of the basic setting, then show how to model contexts, then arbitrary type and term constructors, then signatures, and finally data refinement. This extends and clarifies Kinoshita and Power's work on lax logical relations for call by value languages.

UR - http://www.scopus.com/inward/record.url?scp=58149305591&partnerID=8YFLogxK

UR - http://dx.doi.org/10.1016/j.entcs.2008.12.081

U2 - 10.1016/j.entcs.2008.12.081

DO - 10.1016/j.entcs.2008.12.081

M3 - Article

VL - 225

SP - 281

EP - 302

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

ER -

Axiomatics for Data Refinement in Call by Value Programming Languages

Abstract

Access to Document

Other files and links

Fingerprint

Cite this