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

abstract data typesabstract implementationdata refinementlogical reasoningmodular programmingprogram specificationstructured specificationtype theory

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

• A higher-order calculus and theory abstraction
• Do-it-yourself type theory
• 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?)
• 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

(10)

• A theory for program and data type specification
• A type-theoretic approach to program development
• Abstract Data Types and Type Theory: Theories as Types
• Program derivation in type theory: A partitioning problem
• scientific article; zbMATH DE number 4056978 (Why is no real title available?)
• scientific article; zbMATH DE number 1265030 (Why is no real title available?)
• Circumscription in Data Logic for Data Type Specification
• scientific article; zbMATH DE number 1487738 (Why is no real title available?)
• Classification of control of types in programs with complex data types
• The metatheory of UTT

Describes a project that uses

Uses Software

• Nuprl
• LEGO

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)