Category Theoretic Models of Data Refinement
From MaRDI portal
Publication:4982051
DOI10.1016/j.entcs.2008.12.064zbMath1336.68035OpenAlexW2049194525MaRDI QIDQ4982051
David A. Naumann, Michael Johnson, 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.064
Specification and verification (program logics, model checking, etc.) (68Q60) Categorical logic, topoi (03G30) Categorical semantics of formal languages (18C50) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Predicate transformers and higher-order programs
- Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads
- A calculus of refinements for program derivations
- An algebraic construction of predicate transformers
- Data refinement and algebraic structure
- Soundness of data refinement for a higher-order imperative language
- Forward and backward simulations. I. Untimed Systems
- Data refinement, call by value and higher order programs
- Lax naturality through enrichment
- Proof of correctness of data representations
- Ownership confinement ensures representation independence for object-oriented programs
- The denotational semantics of programming languages
- Some Properties of Predicate Transformers
- A categorical model for higher order imperative programming
- Data Refinement
- Axiomatics for Data Refinement in Call by Value Programming Languages
- Programming Languages and Systems
- Relational Parametricity and Separation Logic
- An algebraic formulation for data refinement
- Predicate transformer semantics of a higher-order imperative language with record subtyping
