Report 2002-1. Activities of the KSU Bioinformatics and Medical Informatics (BMI) Working Group, 2001-2002, by William H. Hsu
Report 2002-2. DUMP: Dump User Memory, Please, by David W. Duffey and Daniel Andresen
Report 2002-3.
Mobile Processes with Dependent Communication Types and
Singleton Types for Names and Capabilities,
by Torben Amtoft and J.B. Wells
Abstract:
There are many calculi for reasoning about concurrent communicating
processes which have locations and are mobile. Examples include the
original Ambient Calculus and its many variants, the Seal Calculus,
the MR-calculus, the M-calculus, etc. It is desirable to use such calculi to
describe the behavior of mobile agents. It seems reasonable that
mobile agents should be able to follow non-predetermined paths and
to carry non-predetermined types of data from location to location,
collecting and delivering this data using communication primitives.
Previous type systems for ambient calculi make this
difficult or impossible to express, because these systems (if they
handle communication at all) have
always globally mapped each ambient name to a type governing the
type of values that can be communicated locally or with adjacent
locations, and this type can not depend on where the ambient has
traveled.
Report 2002-4.
Causal Type System for Ambient Movements,
by Torben Amtoft
Abstract:
The Ambient Calculus was developed by Cardelli and Gordon as a formal framework to study issues of mobility and migrant code. We present a type system for the calculus, parameterized by a set of security constraints: static ones concerning where a given ambient may reside, and dynamic ones expressing where a given ambient may be dissolved. A subject reduction property then guarantees that a well-typed process never violates these constraints; additionally it ensures that communicating subprocesses agree on their ``topic of conversation''.
The type system employs a notion of causality in that processes are assigned ``behaviors''. We argue that this significantly increases the precision of the analysis and compensates for the lack of ``co-capabilities'' (an otherwise increasingly popular extension to the ambient calculus); also it allows (in contrast to other approaches) an ambient to hold multiple topics of conversation.
Based on techniques borrowed from finite automata theory, type checking of type-annotated processes is decidable. Under certain quite natural restrictions, type inference is also possible.