Program specification and data refinement in type theory
DOI10.1017/S0960129500000256zbMATH Open0791.68109OpenAlexW2105528288MaRDI QIDQ4282807FDOQ4282807
Authors: Zhaohui Luo 
Publication date: 14 March 1994
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0960129500000256
Recommendations
type theorymodular programmingprogram specificationabstract data typeslogical reasoningstructured specificationdata refinementabstract implementation
General topics in the theory of software (68N01) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)
Cites Work
- Title not available (Why is that?)
- Proof of correctness of data representations
- The calculus of constructions
- Title not available (Why is that?)
- Title not available (Why is that?)
- Specifications in an arbitrary institution
- Title not available (Why is that?)
- Do-it-yourself type theory
- Structured algebraic specifications: A kernel language
- The extended calculus of constructions (ECC) with inductive types
- Toward formal development of programs from algebraic specifications: Parameterisation revisited
- Type checking with universes
- A higher-order calculus and theory abstraction
Cited In (9)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Abstract Data Types and Type Theory: Theories as Types
- Circumscription in Data Logic for Data Type Specification
- Classification of control of types in programs with complex data types
- The metatheory of UTT
- A theory for program and data type specification
- Title not available (Why is that?)
- Program derivation in type theory: A partitioning problem
Uses Software
This page was built for publication: Program specification and data refinement in type theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4282807)
