[Prev][Next][Index][Thread]
Sussex technical reports
[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]
The following technical reports are now available from our Web
page http://www.cogs.susx.ac.uk.
(96:05) J. Rathke and M. Hennessy: Local Model Checking for a
Value-Based Modal mu-Calculus
Abstract:
We first present a first-order modal mu-calculus which
uses parameterised maximal and minimal fixpoints to describe
safety and liveness
properties of processes which communicate values along ports. Then, using a
class of models based on symbolic graphs, we give a local model checking
proof system for this logic. The system is a natural extension of
existing proof systems and although it is sound it is incomplete in general.
We prove two different completeness results for certain sub-logics.
The first is for safety properties alone, where only parameterised
maximal fixpoints are used while the second allows both kinds of
fixpoints but restricts the use of parameterisation.
(96:04) M. Hennessy: A fully abstract denotational semantics for
the pi-calculus
Abstract:
This paper describes the construction of two set-theoretic
denotational models for the pi-calculus. The models are obtained as
initial solutions to domain equations in a functor category. By
associating with each syntactic construct of the pi-calculus a natural
transformation over these models we obtain two interpretations for the
language.
We also show that these models are FULLY ABSTRACT with respect to
natural behavioural preorders over terms in the language. By this we
mean that two terms are related behaviourally if and only if their
interpretations in the model are related. The behavioural preorders
are the standard versions of MAY and MUST testing adapted to the
pi-calculus.
(96:03) Alan Jeffrey: Semantics for core Concurrent ML using
computation types
Abstract:
This paper presents two typed higher-order concurrent functional
programming languages, based on Reppy's Concurrent ML. The first is a
simplified, monomorphic variant of CML, which allows reduction of
terms of any type. The second uses an explicit type constructor for
computation, in the style of Moggi's monadic metalanguage. Each of
these languages is given an operational semantics, which can be used
as the basis of bisimulation equivalence. We show how Moggi's
translation of the call-by-value lambda-calculus into the mondadic
metalanguage can be extended to these concurrent languages, and that
this translation is correct up to weak bisimulation.
(96:02) W. Ferreira, M. Hennessy and A.S.A. Jeffrey: Combining the
typed lambda-calculus with CCS
Abstract:
We investigate a language obtained by extending the typed
call-by-value lambda calculus with the communication constructs of
CCS. The language contains two interrelated syntactic classes,
processes and expressions. The former are defined using the CCS
constructs of choice, parallelism, and action prefixing of
expressions, where these expressions come from a syntactic class which
also includes the standard constructs from the call-by-value
lambda-calculus. We define a higher order bisimulation equivalence
(95:06) M. Hennessy and H. Lin: Unique fixpoint induction for
message-passing process calculi
Abstract:
We present a proof system for message-passing process calculi with
recursion. The key inference rule to deal with recursive processes is
a version of Unique Fixpoint Induction for process abstractions. We
prove the proof system is sound and also complete for a restricted
form of regular message-passing processes. We also show that the
system is incomplete in general and discuss possible extensions with
inductive inference rules.