Data refinement for call-by-value programming languages. (English) Zbl 0944.68034
Flum, Jörg (ed.) et al., Computer science logic. 13th international workshop, CSL ’99. 8th annual conference of the EACSL, Madrid, Spain, September 20-25, 1999. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1683, 562-576 (1999).
Summary: We give a category theoretic framework for data-refinement in call-by-value programming languages. One approach to data refinement for the simply typed \(\lambda\)-calculus is given by generalizing the notion of logical relation to one of lax logical relation, so that binary lax logical relations compose. So here, we generalize the notion of lax logical relation, defined in category theoretic terms, from the simply typed \(\lambda\)-calculus to the computational \(\lambda\)-calculus as a model of data refinement.
For the entire collection see [Zbl 0929.00039].
For the entire collection see [Zbl 0929.00039].
MSC:
| 68N18 | Functional programming and lambda calculus |
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 03B40 | Combinatory logic and lambda calculus |
| 18D10 | Monoidal, symmetric monoidal and braided categories (MSC2010) |
