Axiomatics for Data Refinement in Call by Value Programming Languages

J Power, M Tanaka

Research output: Contribution to journalArticlepeer-review

148 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 languageEnglish
Pages (from-to)281-302
Number of pages22
JournalElectronic Notes in Theoretical Computer Science
Volume225
DOIs
Publication statusPublished - 2 Jan 2009

Fingerprint Dive into the research topics of 'Axiomatics for Data Refinement in Call by Value Programming Languages'. Together they form a unique fingerprint.

Cite this