Abstract Manes (1998). Implementing Collection Classes with Monads. Mathematical Structures in Computer Science 8 (231–276) introduced the notion of a collection monad on the category of sets as a suitable semantics for collection types. The canonical example of collection monad is the finite powerset monad. In order to account for the algorithmic aspects, the category of sets should be replaced with categories whose arrows are maps computable by low-complexity algorithms. Inspired by realizability, we give a systematic way for constructing categories of small sets and low-complexity functions and define an analogue of collection monads on such categories.

Abstract Robustness is a property of system analyses, namely monotonic maps from the complete lattice of subsets of a (system’s state) space to the two-point lattice. The definition of robustness requires the space to be a metric space. Robust analyses cannot discriminate between a subset of the metric space and its closure; therefore, one can restrict to the complete lattice of closed subsets. When the metric space is compact, the complete lattice of closed subsets ordered by reverse inclusion is $\omega$ -continuous, and robust analyses are exactly the Scott-continuous maps. Thus, one can also ask whether a robust analysis is computable (with respect to a countable base). The main result of this paper establishes a relation between robustness and Scott continuity when the metric space is not compact. The key idea is to replace the metric space with a compact Hausdorff space, and relate robustness and Scott continuity by an adjunction between the complete lattice of closed subsets of the metric space and the $\omega$ -continuous lattice of closed subsets of the compact Hausdorff space. We demonstrate the applicability of this result with several examples involving Banach spaces.

Hybrid systems—more precisely, their mathematical models—can exhibit behaviors, like Zeno behaviors, that are absent in purely discrete or purely continuous systems. First, we observe that, in this context, the usual definition of reachability—namely, the reflexive and transitive closure of a transition relation—can be unsafe, i.e., it may compute a proper subset of the set of states reachable in finite time from a set of initial states. Therefore, we propose safe reachability, which always computes a superset of the set of reachable states. Second, in safety analysis of hybrid and continuous systems, it is important to ensure that a reachability analysis is also robust w.r.t. small perturbations to the set of initial states and to the system itself, since discrepancies between a system and its mathematical models are unavoidable. We show that, under certain conditions, the best Scott continuous approximation of an analysis A is also its best robust approximation. Finally, we exemplify the gap between the set of reachable states and the supersets computed by safe reachability and its best robust approximation.

This paper describes the design and semantics of METAKLAIM, which is a higher order distributed process calculus equipped with staging mechanisms. METAKLAIM integrates METAML (an extension of SML for multi-stage programming) and KLAIM (a Kernel Language for Agents Interaction and Mobility), to permit interleaving of meta-programming activities (such as assembly and linking of code fragments), dynamic checking of security policies at administrative boundaries and ‘traditional’ computational activities on a wide area network (such as remote communication and code mobility). METAKLAIM exploits a powerful type system (including polymorphic types á la system F) to deal with highly parameterised mobile components and to enforce security policies dynamically: types are metadata that are extracted from code at run-time and are used to express trustiness guarantees. The dynamic type checking ensures that the trustiness guarantees of wide area network applications are maintained whenever computations interoperate with potentially untrusted components.

This paper addresses the issue of safely combining computational effects and multi-stage programming. We propose a type system which exploits a notion of closed type , to check statically that an imperative multi-stage program does not cause run-time errors. Our approach is demonstrated formally for a core language called $\hbox{\sf MiniML}^{\sf meta}_{\sf ref}$ . This core language safely combines multi-stage constructs and ML-style references, and is a conservative extension of $\hbox{\sf MiniML}_{\sf ref}$ , a simple imperative subset of SML. In previous work, we introduced a closed type constructor , which was enough to ensure the safe execution of dynamically generated code in the pure fragment of $\hbox{\sf MiniML}^{\sf meta}_{\sf ref}$ .

Launchbury and Peyton Jones came up with an ingenious idea for embedding regions of imperative programming in a pure functional language like Haskell. The key idea was based on a simple modification of Hindley-Milner's type system. Our first contribution is to propose a more natural encapsulation construct exploiting higher-order kinds, which achieves the same encapsulation effect, but avoids the ad hoc type parameter of the original proposal. The second contribution is a type safety result for encapsulation of strict state using both the original encapsulation construct and the newly introduced one. We establish this result in a more expressive context than the original proposal, namely in the context of the higher-order lambda-calculus. The third contribution is a type safety result for encapsulation of lazy state in the higher-order lambda-calculus. This result resolves an outstanding open problem on which previous proof attempts failed. In all cases, we formalize the intended implementations as simple big-step operational semantics on untyped terms, which capture interesting implementation details not captured by the reduction semantics proposed previously.

This special issue reports on some recent advances in the area of intuitionistic modal type theories and their application to Computer Science. It collects a selection of papers presented at the Logic in Computer Science (LICS'99) satellite workshop on Intuitionistic Modal Logics and Applications (IMLA'99) held at Trento, Italy in July 1999. All of the contributors to this one day workshop, which was widely attended, were invited to submit a full and revised version of their papers to this special issue of MSCS. The selection was based on a second round of peer reviewing.

We present an extension of the Hindley–Milner type system that supports a generous class of type constructors called functors, and provide a parametrically polymorphic algorithm for their mapping, i.e. for applying a function to each datum appearing in a value of constructed type. The algorithm comes from shape theory, which provides a uniform method for locating data within a shape. The resulting system is Church–Rosser and strongly normalizing, and supports type inference. Several different semantics are possible, which affects the choice of constants in the language, and are used to illustrate the relationship to polytypic programming.

This paper provides both a fully abstract (domain-theoretic) model for the /spl pi/-calculus and a universal (set-theoretic) model for the finite /spl pi/-calculus with respect to strong late bisimulation and congruence. This is done by: considering categorical models, defining a metalanguage for these models, and translating the /spl pi/-calculus into the metalanguage. A technical novelty of our approach is an abstract proof of full abstraction: The result on full abstraction for the finite /spl pi/-calculus in the set-theoretic model is axiomatically extended to the whole /spl pi/-calculus with respect to the domain-theoretic interpretation. In this proof, a central role is played by the description of non-determinism as a free construction and by the equational theory of the metalanguage.

This paper proposes an internal semantics for the modalities and evaluation predicate of Pitts' Evaluation Logic, and introduces several predicate calculi (ranging from Horn sequents to Higher Order Logic), which are sound and complete w.r.t. natural

The semantics of Evaluation Logic proposed by Moggi (1994) relies on additional properties of monads. This paper proposes an alternative semantics, which drops all additional requirement on monads at the expense of stronger assumptions on the underlying category. These assumptions are satisfied by any topos, but not by the category of cpos. However, in the setting of Synthetic Domain Theory (J. Hyland, 1991) and (P.Taylor, 1991) it is possible to reconcile the needs of denotational semantics with those of logic.>

Various Theories of Types are introduced, by stressing the analogy ‘propositions-as-types’: from propositional to higher order types (and Logic). In accordance with this, proofs are described as terms of various calculi, in particular of polymorphic (second order) λ-calculus. A semantic explanation is then given by interpreting individual types and the collection of all types in two simple categories built out of the natural numbers (the modest sets and the universe of ω-sets). The first part of this paper (syntax) may be viewed as a short tutorial with a constructive understanding of the deduction theorem and some work on the expressive power of first and second order quantification. Also in the second part (semantics, §§6–7) the presentation is meant to be elementary, even though we introduce some new facts on types as quotient sets in order to interpret ‘explicit polymorphism’. (The experienced reader in Type Theory may directly go, at first reading, to §§6–8).

The type-theoretic explanation of modules proposed to date (for programming languages like ML) is unsatisfactory, because it does not capture that the evaluation of type-expressions is independent from the evaluation of program expressions. We propose a new explanation based on ‘programming languages as indexed categories’ and illustrate how ML can be extended to support higher order modules, by developing a category-theoretic semantics for a calculus of modules with dependent types. The paper also outlines a methodology, which may lead to a modular approach in the study of programming languages.

In earlier work, we used a typed function calculus, XML, with dependent types to analyze several aspects of the Standard ML type system. In this paper, we introduce a refinement of XML with a clear compile-time/run-time phase distinction, and a direct compile-time type checking algorithm. The calculus uses a finer separation of types into universes than XML and enforces the phase distinction using a nonstandard equational theory for module and signature expressions. While unusual from a type-theoretic point of view, the nonstandard equational theory arises naturally from the well-known Grothendieck construction on an indexed category.

The lambda -calculus is considered a useful mathematical tool in the study of programming languages. However, if one uses beta eta -conversion to prove equivalence of programs, then a gross simplification is introduced. The author gives a calculus based on a categorical semantics for computations, which provides a correct basis for proving equivalence of programs, independent from any specific computational model.>

The model theory of simply typed and polymorphic (second-order) lambda calculus changes when types are allowed to be empty. For example, the “polymorphic Boolean” type really has exactly two elements in a polymorphic model only if the “absurd” type ∀t.t is empty. The standard β-ε axioms and equational inference rules which are complete when all types are nonempty are not complete for models with empty types. Without a little care about variable elimination, the standard rules are not even sound for empty types. We extend the standard system to obtain a complete proof system for models with empty types. The completeness proof is complicated by the fact that equational “term models” are not so easily obtained: in contrast to the nonempty case, not every theory with empty types is the theory of a single model.

Abstract A type-structure of partial effective functionals over the natural numbers, based on a canonical enumeration of the partial recursive functions, is developed. These partial functionals, defined by a direct elementary technique, turn out to be the computable elements of the hereditary continuous partial objects; moreover, there is a commutative system of enumerations of any given type by any type below (relative numberings). By this and by results in [1] and [2], the Kleene-Kreisel countable functionals and the hereditary effective operations (HEO) are easily characterized.