Software language design and implementation often involve specifications written in various esoteric meta-languages. Language workbenches generally include support for precise name-based navigation when browsing language specifications locally, but such support is lacking when browsing the same specifications online in code repositories.

Specifying and mechanically verifying type safe programming languages requires significant effort. This effort can in theory be reduced by defining and reusing pre-verified, modular components. In practice, however, existing approaches to modular mechanical verification require many times as much specification code as plain, monolithic definitions. This makes it hard to develop new reusable components, and makes existing component specifications hard to grasp. We present an alternative approach based on intrinsically-typed interpreters, which reduces the size and complexity of modular specifications as compared to existing approaches. Furthermore, we introduce a new abstraction for safe-by-construction specification and composition of pre-verified type safe language components: language fragments . Language fragments are about as concise and easy to develop as plain, monolithic intrinsically-typed interpreters, but require about 10 times less code than previous approaches to modular mechanical verification of type safety.

The programming and modelling languages currently used in software engineering generally have plenty of tool support. But although their syntax is specified using formal grammars or meta-models, complete formal semantic specifications are seldom provided.

Dealing with polymorphism in the presence of imperative features is a long-standing open problem for Hindley-Milner type systems. A widely adopted approach is the value restriction, which inhibits polymorphic generalisation and unfairly rejects various programs that cannot go wrong. We consider abstract interpretation as a tool for constructing safe and precise type systems, and investigate how to derive store-based types by abstract interpretation. We propose store-based types as a type discipline that holds potential for interesting and flexible alternatives to the value restriction.

Abstract The Vienna Development Method (VDM) was developed in the early 1970s as a variant of denotational semantics. VDM descriptions of programming languages differ from the original Scott–Strachey style by making extensive use of combinators which have a fixed operational interpretation. After recalling the main features of denotational semantics and the Scott–Strachey style, we examine the combinators of the VDM specification language, and relate them to monads, which were introduced more than 15 years later. We also suggest that use of further monadic combinators in VDM could be beneficial. Finally, we provide an overview of published VDM semantic descriptions of major programming languages.

In most algebraic specification frameworks, the type system is restricted to sorts, subsorts, and first‐order function types. This is in marked contrast to the so‐called model‐oriented frameworks, which provide higher‐order types, interpreted set‐theoretically as Cartesian products, function spaces, and power‐sets. This paper presents a simple framework for algebraic specifications with higher‐order types and set‐theoretic models. It may be regarded as the basis for a Horn‐clause approximation to the Z framework, and has the advantage of being amenable to prototyping and automated reasoning. Standard set‐theoretic models are considered, and conditions are given for the existence of initial reducts of such models. Algebraic specifications for various set‐theoretic concepts are considered.

A framework for algebraic specification of abstract data types is introduced. It involves so-called unified algebras, where sorts are treated as values, so that operations can be applied to sorts as well as to the elements that they classify. An institution for unified algebras is defined and shown to be liberal. However, the ordinary forgetful functor does not forget any values in unified algebras, so the usual data constraints do not have any models. A more forgetful functor is introduced and used to define so-called bounded data constraints, which have the expected models.>

This paper concerns the algebraic specification of abstract data types. It introduces and motivates the recently-developed framework of unified algebras, and provides a practical notation for their modular specification. It also compares unified algebras with the well-known framework of order-sorted algebras, which underlies the OBJ specification language.

We give two proofs of Wadsworth’s classic approximation theorem for the pure $\lambda $-calculus. One of these illustrates a new method utilising a certain kind of intermediate semantics for proving correspondences between denotational and operational semantics. The other illustrates a direct technique of Milne, employing recursively-specified inclusive relations.