Browsing Informatics, School of by Publication Type "Preprint"
Now showing items 120 of 32

Abstract Syntax and Variable Binding (Extended Abstract)
(20031106)We develop a theory of abstract syntax with variable binding. To every binding signature we associate a category of models consisting of variable sets endowed with compatible algebra and substitution structures. The ... 
Adequacy for Algebraic Effects
(SPRINGERVERLAG, 2002)Moggi proposed a monadic account of computational effects. He also presented the computational lamdacalculus, c, a core callbyvalue functional programming language for effects; the effects are obtained by adding ... 
An Axiomatisation of Computationally Adequate Domain Theoretic Models of FPC
(1994)Categorical models of the metalanguage FPC (a type theory with sums, products, exponentials and recursive types) are defined. Then, domaintheoretic models of FPC are axiomatised and a wide subclass of them —the ... 
Bialgebraic Semantics and Recursion
(Elsevier Science, 2001)In [9] a unifying framework was given for operational and denotational semantics. It uses bialgebras, which are combinations of algebras (used for syn tax and denotational semantics) and coalgebras (used for operational ... 
Combining computational effects: commutativity and sum
(20031105)We begin to develop a unified account of modularity for computational effects. We use the notion of enriched Lawvere theory, together with its relationship with strong monads, to reformulate Moggi’s paradigm for modelling ... 
Complete Cuboidal Sets in Axiomatic Domain Theory (Extended Abstract)
(20031106)We study the enrichment of models of axiomatic do main theory. To this end, we introduce a new and broader notion of domain, viz. that of complete cuboidal set, that complies with the axiomatic requirements. We show ... 
Computational effects and operations: an overview
(2002)We overview a programme to provide a unified semantics for computational effects based upon the notion of a countable enriched Lawvere theory. We define the notion of countable enriched Lawvere theory, show how the various ... 
Concrete Domains
(1993)This paper introduces the theory of a particular kind of computation domains called concrete domains. The purpose of this theory is to find a satisfactory framework for the notions of coroutine computation and sequentiality ... 
Configuration Structures
(20031105)In this paper the correspondence between safe Petri nets and event structures, due to Nielsen, Plotkin and Winskel, is extended to arbitrary nets without selfloops, under the collective token interpretation. To this ... 
An Extension of Models of Axiomatic Domain Theory to Models of Synthetic Domain Theory
(20031105)We relate certain models of Axiomatic Domain Theory (ADT) and Synthetic Domain Theory (SDT). On the one hand, we introduce a class of nonelementary models of SDT and show that the domains in them yield models of ADT. ... 
FAITHFUL IDEAL MODELS FOR RECURSIVE POLYMORPHIC TYPES
(20031103)We explore ideal models for a programming language with recursive polymorphic types, variants of the model studied by MacQueen, Plotkin, and Sethi. The use of suitable ideals yields a close fit between models and programming ... 
A Framework for Defining Logics
(ASSOC COMPUTING MACHINERY, NEW YORK, 1993)The Edinburgh Logical Framework (LF) provides a means to define (or present) logics. It is based on a general treatment of syntax, rules, and proofs by means of a typed λcalculus with dependent types. Syntax is treated ... 
From Action Calculi to Linear Logic
(SPRINGERVERLAG, 1998)Milner introduced action calculi as a framework for investigating models of interactive behaviour. We present a typetheoretic account of action calculi using the propositionsastypes paradigm; the type theory has a ... 
Full Abstraction, Totality and PCF
(20031106)Inspired by a question of Riecke, we consider the interaction of totality and full abstraction, asking whether full abstraction holds for Scott’s model of cpos and continuous functions if one restricts to total programs ... 
An Illative Theory of Relations
(20031103)In a previous paper an intensional theory of relations was formulated [Plo90]. It was intended as a formalisation of some of the ideas of Situation Theory concerning relations, assignments, statesofa airs and facts; ... 
Lax Logical Relations
(SPRINGERVERLAG, 2000)Lax logical relations are a categorical generalisation of logical relations; though they preserve product types, they need not preserve exponential types. But, like logical relations, they are preserved by the meanings ... 
A Logic for Parametric Polymorphism
(20031105)In this paper we introduce a logic for parametric polymorphism. Just as LCF is a logic for the simplytyped calculus with recursion and arithmetic, our logic is a logic for System F. The logic permits the formal ... 
Logical Full Abstraction and PCF
(2000)We introduce the concept of logical full abstraction, generalising the usual equational notion. We consider the language PCF and two extensions with “parallel” operations. The main result is that, for standard ... 
A Logical View of Composition
(20031105)We define two logics of safety specifications for reactive systems. The logics provide a setting for the study of composition rules. The two logics arise naturally from extant specification approaches; one of the logics ... 
Notions of Computation Determine Monads
(SPRINGERVERLAG, 2002)We model notions of computation using algebraic operations and equations. We show that these generate several of the monads of pri mary interest that have been used to model computational e ects, with the striking ...