Program specification and data refinement in type theory

DOI10.1017/S0960129500000256zbMath0791.68109OpenAlexW2105528288MaRDI QIDQ4282807

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

zbMATH Keywords

program specificationdata refinementtype theorylogical reasoningmodular programmingabstract data typesstructured specificationabstract implementation

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) General topics in the theory of software (68N01)

Related Items (1)

The metatheory of UTT

Uses Software

• Nuprl
• LEGO

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Do-it-yourself type theory
• Structured algebraic specifications: A kernel language
• The calculus of constructions
• Specifications in an arbitrary institution
• Type checking with universes
• The extended calculus of constructions (ECC) with inductive types
• Toward formal development of programs from algebraic specifications: Parameterisation revisited
• Proof of correctness of data representations
• A higher-order calculus and theory abstraction

This page was built for publication: Program specification and data refinement in type theory