Journal Article Computable Models Get access Raymond Turner Raymond Turner Department of Computer Science, The University of Essex, UK. Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 18, Issue 2, April 2008, Pages 283–318, https://doi.org/10.1093/logcom/exm002 Published: 03 March 2007 Article history Received: 26 January 2006 Published: 03 March 2007

In reference (Foundation of specification. Journal of Logic and Computation, 15, 951–974, 2005), the author introduces a core specification theory (CST) in order to provide a logical framework for the design and exploration of specification languages. In this article, we formulate two highly expressive extensions of CST. The first (CSTU) is CST + a universe of types and the second (CSTUS) permits specifications themselves to be data items. Finally, we shall explore their metamathematical properties and, in particular, provide an interpretation into first-order arithmetic.

This is a continuation of a paper in which the role of types in semantic theory was explored. Inevitably, in that paper some issues in type theory and semantics were treated only in passing. In particular, little was said about Stratified Type Theories. This paper concentrates on these theories and provides a theoretical framework for semantic applications.

We develop and explore a Core Specification Theory(CST) as a basis for the meta-mathematical investigation of specification and specification languages.

YPA (Yellow Pages Assistant) is a telephone directory enquiry system that allows a user to access addresses and other advertiser information in a classified directory. BT's Yellow Pages provide an example of a classified directory with which this work would be useful.

The underlying set theory of the Z-specification language is said to be a typed set theory. There are two interpretations of this to be found in the literature. One is based upon Simple Type theory and the other on set theory plus a type assignment system. We establish their equivalence.

An approach to Z-style program specification is developed based upon a constructive version of Zermelo-Fraenkel set theory without replacement. The idea of obligation schema, an extension of Z-schema, is introduced, and an implementation of this notion presented which facilitates the abstraction of programs.

We formulate and investigate various ways of (conservatively) extending Martin-Löf's type theories with separation types and choice principles and demonstrate how these extenstions can be employed to formalize Bishop's mathematical practice of hiding and recovering witnessing information.

In this paper we develop and explore some constructive theories of operations and types aimed at providing a foundation for constructive functional programming. More specifically, we develop theories which are highly expressive but computationally weak. In particular, the final theories of the paper have the computational strength of primitive recursive arithmetic.

Two foundational systems have been employed to provide the underlying foundations for constructive functional programming (CFP). Neither of these theories was designed with CFP as its major area of application. Our goal is to set the scene for the design of such a theory. This will involve a detailed comparison of the two from the perspective of CFP. The paper contains a series of constructive theories of operations, types and termination, each member of which concentrates upon one particular issue in the design process.

An introduction is given to the use of formal semantics as a means of both specifying relational query languages and of establishing a conceptual basis for their analysis. The approach is demonstrated with respect to the relational calculus and then extended to cope with the more advanced constructs of SEQUEL and QUEL.