A theory for program and data type specification
type: Item
instance of: scholarly article
title: A theory for program and data type specification
zbMATH Open document ID: 0759.68061
DOI: 10.1016/0304-3975(92)90169-G
published in: Theoretical Computer Science
publication date: 1993-01-17T00:00:00Z
review text: This is an attempt to develop a wide spectrum formalism which will support not only reasoning about program equivalence, but also covers reasoning about some properties of computations, specifications of programs and data types. The first-order, two-layered theory which is called IOCC (impredective theory of operations, control and classes) was created for these purposes. The lower layer is a theory of program equivalence and definedness. The upper layer is a theory of class membership with a general principle for defining classes. Examples are given to illustrate the reasoning about programs, steams and coroutines.
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 96274
zbMATH Keywords: program equivalence
zbMATH Keywords: reasoning about programs
author: Carolyn Talcott
reviewed by: Anatoly V. Anisimov
describes a project that uses: ALGOL 60
describes a project that uses: LISP
MaRDI profile type: Publication
cites work: Q3686011
cites work: Q3679172
cites work: Partial abstract types
cites work: On the algebraic definition of programming languages
cites work: Stream Processing Functions
cites work: Design of a separable transition-diagram compiler
cites work: Q3709890
cites work: Q4128540
cites work: Q3882452
cites work: Q3663255
cites work: Q4723729
cites work: Q3478384
cites work: A syntactic theory of sequential control
cites work: The revised report on the syntactic theories of sequential control and state
cites work: A simplifier for untyped lambda expressions
cites work: Correspondence between ALGOL 60 and Church's Lambda-notation
cites work: The next 700 programming languages
cites work: Q4124327
cites work: Q3202991
cites work: Call-by-name, call-by-value and the \(\lambda\)-calculus
cites work: Q5685626
cites work: Q3997095
cites work: Scheme: A interpreter for extended lambda calculus
full work available at URL: 0304-3975(92)90169-g
OpenAlex ID: W2012140088
Recommended article: Program specification and data refinement in type theory
Recommended article: A type-theoretic approach to program development
Recommended article: Q3323252
Recommended article: Q4016523
Recommended article: Q4723729
Recommended article: Abstract Data Types and Type Theory: Theories as Types
Recommended article: Data type specification
Recommended article: Q3476793
Recommended article: First-order specifications of programmable data types
description: scientific article; zbMATH DE number 96274