Edinburgh Research Archive

Moggi proposed a monadic account of computational effects. He also presented the computational lamda-calculus, c, a core call-by-value functional programming language for effects; the effects are obtained by adding ...

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 ...

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 ...

We study some of the concepts, protocols, and algorithms for access control in distributed systems, from a logical perspective. We account for how a principal may come to believe that another principal is making a request, ...

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 ...

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 ...

Categorical models of the metalanguage FPC (a type theory with sums, products, exponentials and recursive types) are defined. Then, domain-theoretic models of FPC are axiomatised and a wide subclass of them —the ...

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 ...

We relate certain models of Axiomatic Domain Theory (ADT) and Synthetic Domain Theory (SDT). On the one hand, we introduce a class of non-elementary models of SDT and show that the domains in them yield models of ADT. ...

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, states-of-a airs and facts; ...