Program specification and data refinement in type theory

DOI10.1017/S0960129500000256MaRDI QIDQ4282807zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

type theorymodular programmingprogram specificationabstract data typeslogical reasoningstructured specificationdata refinementabstract implementation

Mathematics Subject Classification ID

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

Recommendations

• Program development in constructive type theory
• Program derivation in type theory: A partitioning problem
• Propositions and specifications of programs in Martin-Löf's type theory
• scientific article; zbMATH DE number 1678369
• A theory for program and data type specification

Cites work

• scientific article; zbMATH DE number 3888893 (Why is no real title available?)
• scientific article; zbMATH DE number 3936465 (Why is no real title available?)
• scientific article; zbMATH DE number 44486 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• A higher-order calculus and theory abstraction
• Do-it-yourself type theory
• Proof of correctness of data representations
• Specifications in an arbitrary institution
• Structured algebraic specifications: A kernel language
• The calculus of constructions
• The extended calculus of constructions (ECC) with inductive types
• Toward formal development of programs from algebraic specifications: Parameterisation revisited
• Type checking with universes

Cited in

(9)

• scientific article; zbMATH DE number 1487738 (Why is no real title available?)
• scientific article; zbMATH DE number 4056978 (Why is no real title available?)
• 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
• scientific article; zbMATH DE number 1265030 (Why is no real title available?)
• Program derivation in type theory: A partitioning problem

Describes a project that uses

Uses Software

• LEGO
• Nuprl

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)