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

The connection between operational and denotational semantics is of longstanding interest in the study of programming languages. One naturally seeks positive results. For example in [FP94, Sim99] adequacy results are ...

Curry’s system for F-deducibility is the basis for static type inference algorithms for programming languages such as ML. If a natural “preservation of types by conversion” rule is added to Curry’s system, it becomes ...

Given a model of the polymorphic typed lambda calculus based upon a Cartesian closed category K, there will be functors from K to K whose action on objects can be expressed by type expressions and whose action on morphisms ...

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

In this paper we introduce a logic for parametric polymorphism. Just as LCF is a logic for the simply-typed -calculus with recursion and arithmetic, our logic is a logic for System F. The logic permits the formal ...

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

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

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