Sharing Implementations of Graph Rewriting Systems

Sharing graphs are a brilliant solution to the implementation of Lévy optimal reductions of λ-calculus. Sharing graphs are interesting on their own and optimal sharing reductions are just a particular reduction strategy of a more general sharing reduction system.The paper is a gentle introduction to sharing graphs and tries to confute some of the common myths on the difficulty of sharing implementations.     

Token-Passing Nets: Call-by-Need for Free

Recently, encodings in interaction nets of the call-by-name and call-by-value strategies of the λ-calculus have been proposed. The purpose of these encodings was to bridge the gap between interaction nets and traditional abstract machines, which are both used to provide lower-level specifications of strategies of the λ-calculus, but in radically different ways. The strength of these encodings is their simplicity, which comes from the simple idea of introducing an explicit syntactic object to represent the flow of evaluation. In particular, no artifact to represent boxes is needed. However, these encodings purposefully follow as closely as possible the implemented strategies, call-by-name and call-by-value, hence do not benefit from the ability of interaction nets to easily represent sharing. The aim of this note is to show that sharing can indeed be achieved without adding any structure. We thus present the call-by-need strategy following the same philosophy, which is indeed not any more complicated than call-by-name. This continues the task of bridging the gap between interaction nets and abstract machines, thus pushing forward a more uniform framework for implementations of the λ-calculus.     

Strong normalisation in the π-calculus

We introduce a typed π-calculus where strong normalisation is ensured by typability. Strong normalisation is a useful property in many computational contexts, including distributed systems. In spite of its simplicity, our type discipline captures a wide class of converging name-passing interactive behaviour. The proof of strong normalisability combines methods from typed λ-calculi and linear logic with process-theoretic reasoning. It is adaptable to systems involving state, non-determinism, polymorphism, control and other extensions. Strong normalisation is shown to have significant consequences, including finite axiomatisation of weak bisimilarity, a fully abstract embedding of the simply typed λ-calculus with products and sums and basic liveness in interaction. Strong normalisability has been extensively studied as a fundamental property in functional calculi, term rewriting and logical systems. This work is one of the first steps to extend theories and proof methods for strong normalisability to the context of name-passing processes.     

Compositional characterisations of -terms using intersection types

We show how to characterise compositionally a number of evaluation properties of λ-terms using Intersection Type assignment systems. In particular, we focus on termination properties, such as strong normalisation, normalisation, head normalisation, and weak head normalisation. We consider also the persistent versions of such notions. By way of example, we consider also another evaluation property, unrelated to termination, namely reducibility to a closed term.Many of these characterisation results are new, to our knowledge, or else they streamline, strengthen, or generalise earlier results in the literature.The completeness parts of the characterisations are proved uniformly for all the properties, using a set-theoretical semantics of intersection types over suitable kinds of stable sets. This technique generalises Krivine's and Mitchell's methods for strong normalisation to other evaluation properties.     

一种基于问题求解理论的密码协议形式模型

提出了一种基于问题求解理论的密码协议模型，给出了模型的基本语法以及基于ρ演算的形式语义，明确了模型推理过程中涉及到的一些关键性的概念和命题。该模型具有以下特点：能够对密码协议进行精确的形式化描述；具有合理可靠的可证明语义；对密码协议安全性的定义精确合理；便于实现自动化推理。所有这些均确保了基于该模型的密码协议安全性分析的合理性和有效性，为正确的分析密码协议的安全性提供了可靠依据。     

Do-it-yourself type theory

This paper provides a tutorial introduction to a constructive theory of types based on, but incorporating some extensions to, that originally developed by Per Martin-Löf. The emphasis is on the relevance of the theory to the construction of computer programs and, in particular, on the formal relationship between program and data structure. Topics discussed include the principle of propositions as types, free types, congruence types, types with information loss and mutually recursive types. Several examples of program development within the theory are also discussed in detail.     

A Guided Tour through some Extensions of the Event Calculus

Kowalski and Sergot's Event Calculus (EC) is a simple temporal formalism that, given a set of event occurrences, derives the maximal validity intervals (MVIs) over which properties initiated or terminated by these events hold. In this paper, we conduct a systematic analysis of EC by which we gain a better understanding of this formalism and determine ways of augmenting its expressive power. The keystone of this endeavor is the definition of an extendible formal specification of its functionalities. This formalization has the effects of casting determination of MVIs as a model checking problem, of setting the ground for studying and comparing the expressiveness and complexity of various extensions of EC, and of establishing a semantic reference against which to verify the soundness and completeness of implementations. We extend the range of queries accepted by EC, which is limited to Boolean combinations of MVI verification or computation requests, to support arbitrary quantification over events and modal queries. We also admit specifications based on preconditions. We demonstrate the added expressive power by encoding a number of diagnosis problems. Moreover, we provide a systematic comparison of the expressiveness and complexity of the various extended event calculi against each other. Finally, we propose a declarative encoding of these enriched event calculi in the logic programming language λProlog and prove the soundness and completeness of the resulting logic programs.     

UppDMC: A Distributed Model Checker for Fragments of the μ-Calculus

We present UppDMC, a distributed model-checking tool. It is tailored for checking finite-state systems and μ-calculus specifications with at most one alternation of minimal and maximal fixed-point operators. This fragment is also known as . Recently, efficient game-based algorithms for this logic have been outlined.We describe the implementation of these algorithms within UppDMC and study their performance on practical examples. Running UppDMC on a simple workstation cluster, we were able to check liveness properties of the largest examples given in the VLTS Benchmark Suite, for which no answers were previously known.     

A Formal Framework for Web Services Coordination

Recently the term Web Services Choreography has been introduced to address some issues related to Web Services Composition and Coordination. Several proposals for describing Choreography for Business Processes have been presented in the last years and many of these languages (e.g. BPEL4WS) make use of concepts as long-running transactions and compensations for coping with error handling. However, the complexity of BPEL4WS makes it difficult to formally define this framework, thus limiting the formal reasoning about the designed applications. In this paper, we formally address Web Services Coordination with particular attention to Web transactions. We enhance our past work - the Event Calculus - introducing two main novelties: i) a multicast event notification mechanism, and ii) event scope names binding. The former enables an easier specification of complex coordination scenarios — such as E-commerce applications require — while the latter allows many new interesting behaviors which can be very useful in business scenarios: the introduction of private event scope names — used to deal with security and privacy — and a dynamic event scopes definition that can be used to manage multiple instances of the same application.     

Interfaces as functors, programs as coalgebras—A final coalgebra theorem in intensional type theory

In [P. Hancock, A. Setzer, Interactive programs in dependent type theory, in: P. Clote, H. Schwichtenberg (Eds.), Proc. 14th Annu. Conf. of EACSL, CSL’00, Fischbau, Germany, 21–26 August 2000, Vol. 1862, Springer, Berlin, 2000, pp. 317–331, URL citeseer.ist.psu.edu/article/hancock00interactive.html; P. Hancock, A. Setzer, Interactive programs and weakly final coalgebras in dependent type theory, in: L. Crosilla, P. Schuster (Eds.), From Sets and Types to Topology and Analysis. Towards Practicable Foundations for Constructive Mathematics, Oxford Logic Guides, Clarendon Press, 2005, URL www.cs.swan.ac.uk/csetzer/] Hancock and Setzer introduced rules to extend Martin-Löf's type theory in order to represent interactive programming. The rules essentially reflect the existence of weakly final coalgebras for a general form of polynomial functor. The standard rules of dependent type theory allow the definition of inductive types, which correspond to initial algebras. Coalgebraic types are not represented in a direct way. In this article we show the existence of final coalgebras in intensional type theory for these kind of functors, where we require uniqueness of identity proofs () for the set of states and the set of commands which determine the functor. We obtain the result by identifying programs which have essentially the same behaviour, viz. are bisimular. This proves the rules of Setzer and Hancock admissible in ordinary type theory, if we replace definitional equality by bisimulation. All proofs [M. Michelbrink, Verifications of final coalgebra theorem in: Interfaces as Functors, Programs as Coalgebras—A Final Coalgebra Theorem in Intensional Type Theory, 2005, URL www.cs.swan.ac.uk/csmichel/] are verified in the theorem prover agda [C. Coquand, Agda, Internet, URL www.cs.chalmers.se/catarina/agda/; K. Peterson, A programming system for type theory, Technical Report, S-412 96, Chalmers University of Technology, Göteborg, 1982], which is based on intensional Martin-Löf type theory.     

Models for name-passing processes: interleaving and causal

We study syntax-free models for name-passing processes. For interleaving semantics, we identify the indexing structure required of an early labelled transition system to support the usual π-calculus operations, defining Indexed Labelled Transition Systems. For non-interleaving causal semantics we define Indexed Labelled Asynchronous Transition Systems, smoothly generalizing both our interleaving model and the standard Asynchronous Transition Systems model for CCS-like calculi. In each case we relate a denotational semantics to an operational view, for bisimulation and causal bisimulation respectively. We establish completeness properties of, and adjunctions between, categories of the two models. Alternative indexing structures and possible applications are also discussed. These are first steps towards a uniform understanding of the semantics and operations of name-passing calculi.     

Type Theory and Language Constructs for Objects with States

In current class-based Object-Oriented Programming Languages (OOPLs), object types include only static features. How to add object dynamic behaviors modeled by Harel's statecharts into object types is a challenging task. We propose adding states and state transitions, which are largely unstated in object type theory, into object type definitions and typing rules. We argue that dynamic behaviors of objects should be part of object type definitions. We propose our type theory, the τ-calculus, which refines Abadi and Cardelli's ζ-calculus, in modeling objects with their dynamic behaviors. In our proposed type theory, we also explain that a subtyping relation between object types should imply the inclusion of their dynamic behaviors. By adding states and state transitions into object types, we propose modifying programming language constructs for state tracking.     

A formalised first-order confluence proof for the λ-calculus using one-sorted variable names

We present the titular proof development that has been verified in Isabelle/HOL. As a first, the proof is conducted exclusively by the primitive proof principles of the standard syntax and of the considered reduction relations: the naive way, so to speak. Curiously, the Barendregt Variable Convention takes on a central technical role in the proof. We also show: (i) that our presentation of the λ-calculus coincides with Curry’s and Hindley’s when terms are considered equal up to α-equivalence and (ii) that the confluence properties of all considered systems are equivalent.     

Biological Transactions for Quantitative Models

In this work an extension of stochastic π-calculus with biological transactions is presented. This permits to model multi-reactant multi-product reactions as atomic actions when quantitative information are given. First, the syntax and the semantics are defined, then some transaction properties are discussed. Finally, some examples are described.     

Structured coalgebras and minimal HD-automata for the -calculus

The coalgebraic framework developed for the classical process algebras, and in particular its advantages concerning minimal realizations, does not fully apply to the π-calculus, due to the constraints on the freshly generated names that appear in the bisimulation.In this paper we propose to model the transition system of the π-calculus as a coalgebra on a category of name permutation algebras and to define its abstract semantics as the final coalgebra of such a category. We show that permutations are sufficient to represent in an explicit way fresh name generation, thus allowing for the definition of minimal realizations.We also link the coalgebraic semantics with a slightly improved version of history dependent (HD) automata, a model developed for verification purposes, where states have local names and transitions are decorated with names and name relations. HD-automata associated with agents with a bounded number of threads in their derivatives are finite and can be actually minimized. We show that the bisimulation relation in the coalgebraic context corresponds to the minimal HD-automaton.     

A complete system for the intelligent interpretation of engineering drawings

Converting paper-based engineering drawings into CAD model files is a tedious process. Therefore, automating the conversion of such drawings represents tremendous time and labor savings. We present a complete system which interprets such 2D paper-based engineering drawings, and outputs 3D models that can be displayed as wireframes. The system performs the detection of dimension sets, the extraction of object lines, and the assembly of 3D objects from the extracted object lines. A knowledge-based method is used to remove dimension sets and text from ANSI engineering drawings, a graphics recognition procedure is used to extract complete object lines, and an evidential rule-based method is utilized to identify view relationships. While these methods are the subject of several of our previous papers, this paper focuses on the 3D interpretation of the object. This is accomplished using a technique based on evidential reasoning and a wide range of rules and heuristics. The system is limited to the interpretation of objects composed of planar, spherical, and cylindrical surfaces. Experimental results are presented. Received December 2, 1998 / Revised June 18, 1999     

A Proof Search Specification of the π-Calculus

We present a meta-logic that contains a new quantifier (for encoding “generic judgments”) and inference rules for reasoning within fixed points of a given specification. We then specify the operational semantics and bisimulation relations for the finite π-calculus within this meta-logic. Since we restrict to the finite case, the ability of the meta-logic to reason within fixed points becomes a powerful and complete tool since simple proof search can compute this one fixed point. The quantifier helps with the delicate issues surrounding the scope of variables within π-calculus expressions and their executions (proofs). We shall illustrate several merits of the logical specifications we write: they are natural and declarative; they contain no side conditions concerning names of variables while maintaining a completely formal treatment of such variables; differences between late and open bisimulation relations are easy to see declaratively; and proof search involving the application of inference rules, unification, and backtracking can provide complete proof systems for both one-step transitions and for bisimulation.     

A Behavioural Pseudometric based on λ–Bisimilarity

In order to describe approximate equivalence among processes, the notions of λ–bisimilarity and behavioural pseudometric have been introduced by Ying and van Breugel respectively. Van Breugel provides a distance function induced by λ–bisimilarity, and conjectures that his behavioural pseudometric coincides with this function. This paper is inspired by this conjecture. We give a negative answer for van Breugel's conjecture first. Moreover, we show that the distance function induced by λ–bisimilarity is a pseudometric on states, and provide a fixed point characterization of this pseudometric.