Data refinement, call by value and higher order programs

David A. Naumann

doi:10.1007/BF01210999

Data refinement, call by value and higher order programs

David A. Naumann

Department of Computer Science

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

8 Scopus citations

Abstract

Using 2-categorical laws of algorithmic refinement, we show soundness of data refinement for stored programs and hence for higher order procedures with value/result parameters. The refinement laws hold in a model that slightly generalizes the standard predicate transformer semantics for the usual imperative programming constructs including prescriptions.

Original language	English
Pages (from-to)	652-662
Number of pages	11
Journal	Formal Aspects of Computing
Volume	7
Issue number	6
DOIs	https://doi.org/10.1007/BF01210999
State	Published - Nov 1995

Keywords

Data refinement
Higher types
Lax exponent
Predicate transformers
Programming calculi
Refinement calculus

Access to Document

10.1007/BF01210999

Cite this

@article{d76055365405427f94b2358fa567e7f8,

title = "Data refinement, call by value and higher order programs",

abstract = "Using 2-categorical laws of algorithmic refinement, we show soundness of data refinement for stored programs and hence for higher order procedures with value/result parameters. The refinement laws hold in a model that slightly generalizes the standard predicate transformer semantics for the usual imperative programming constructs including prescriptions.",

keywords = "Data refinement, Higher types, Lax exponent, Predicate transformers, Programming calculi, Refinement calculus",

author = "Naumann, {David A.}",

year = "1995",

month = nov,

doi = "10.1007/BF01210999",

language = "English",

volume = "7",

pages = "652--662",

number = "6",

}

TY - JOUR

T1 - Data refinement, call by value and higher order programs

AU - Naumann, David A.

PY - 1995/11

Y1 - 1995/11

N2 - Using 2-categorical laws of algorithmic refinement, we show soundness of data refinement for stored programs and hence for higher order procedures with value/result parameters. The refinement laws hold in a model that slightly generalizes the standard predicate transformer semantics for the usual imperative programming constructs including prescriptions.

AB - Using 2-categorical laws of algorithmic refinement, we show soundness of data refinement for stored programs and hence for higher order procedures with value/result parameters. The refinement laws hold in a model that slightly generalizes the standard predicate transformer semantics for the usual imperative programming constructs including prescriptions.

KW - Data refinement

KW - Higher types

KW - Lax exponent

KW - Predicate transformers

KW - Programming calculi

KW - Refinement calculus

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

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

U2 - 10.1007/BF01210999

DO - 10.1007/BF01210999

M3 - Article

AN - SCOPUS:0000745709

SN - 0934-5043

VL - 7

SP - 652

EP - 662

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

IS - 6

ER -

Data refinement, call by value and higher order programs

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this