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