Axiomatics for Data Refinement in Call by Value Programming Languages

DOI10.1016/j.entcs.2008.12.081zbMath1336.68032OpenAlexW1984439283MaRDI QIDQ4982069

Miki Tanaka, A. John Power

Publication date: 23 March 2015

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2008.12.081

zbMATH Keywords

data refinementcomputational lambda calculuspremonoidal categoryLax logical relation

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18) Categorical semantics of formal languages (18C50) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

Category Theoretic Models of Data Refinement

Cites Work

• Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads
• Generic models for computational effects
• Two-dimensional monad theory
• A representable approach to finite nondeterminism
• Data refinement and algebraic structure
• Premonoidal categories as categories with algebraic structure
• Sketches
• Proof of correctness of data representations
• On MacLane's conditions for coherence of natural associativities, commutativities, etc
• Premonoidal categories and notions of computation
• Types, abstraction, and parametric polymorphism, part 2
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Axiomatics for Data Refinement in Call by Value Programming Languages