Foundations of Software Science and Computation Structures

Genericity is the idea that the same program can work at many different data types.Longo,Milsted and Soloviev proposed to capture the inability of generic programs to probe the structure of their instances by the following equational principle:if two generic programs, viewed as terms of type.∀X.A [X ],are equal at any given instance A [T ], then they are equal at all instances.They proved that this rule is admissible in a certain extension of System F,but finding a semantically motivated model satisfying this principle remained an open problem. In the present paper,we construct a categorical model of polymorphism, based on game semantics,which contains a large collection of generic types.This model builds on two novel constructions: - A direct interpretation of variable types as games,with a natural notion of substitution of games.This allows moves in games A [T ]to be decomposed into the generic part from A ,and the part pertaining to the instance T .This leads to a simple and natural notion of generic strategy. - A “relative polymorphic product”π _i(A,B)which expresses quantification over the type variable X _i in the variable type A with respect to a “universe” which is explicitly given as an additional parameter B .We then solve a recursive equation involving this relative product to obtain a universe in a suitably “absolute” sense.

Full Completeness for ML types (universal closures of quantifier-free types)can be proved for this model.

We introduce the notion of containers as a mathematical formalisation of the idea that many important datatypes consist of templates where data is stored. We show that containers have good closure properties under a variety of constructions including the formation of initial algebras and final coalgebras. We also show that containers include strictly positive types and shapely types but that there are containers which do not correspond to either of these. Further, we derive a representation result classifying the nature of polymorphic functions between containers. We finish this paper with an application to the theory of shapely types and refer to a forthcoming paper which applies this theory to differentiable types.

We solve the problem of extending Bird and Paterson’s generalized folds for nested datatypes and its dual to inductive and coinductive constructors of arbitrarily high ranks by appropriately generalizing Mendler-style (co)iteration.Characteristically to Mendler-style schemes of disciplined (co)recursion,the schemes we propose do not rest on notions like positivity or monotonicity of a constructor and facilitate programming in a natural and elegant style close to programming with the customary letrec construct,where the typings of the schemes,however, guarantee termination. For rank 2,a smoothened version of Bird and Paterson's generalized folds and its dual are achieved;for rank 1,the schemes instantiate to Mendler's original (re)formulation of iteration and coiteration. Several examples demonstrate the power of the approach. Strong normalization of our proposed extension of system F ^ω of higher-order parametric polymorphism is proven by a reduction-preserving embedding into pure F ^ω.

Every parity game is a combinatorial representation of a closed Boolean μ-term. When interpreted in a distributive lattice every Boolean μ-term is equivalent to a fixed-point free term. The alternationdepth hierarchy is therefore trivial in this case. This is not the case for non distributive lattices, as the second author has shown that the alternation -depth hierarchy is infinite.

In this paper we show that the alternation-depth hierarchy of the games μ-calculus, with its interpretation in the class of all complete lattices, has a nice characterization of ambiguous classes: every parity game which is equivalent both to a game in σ_n+1 and to a game π_n+1 is also equivalent to a game obtained by composing games in σ_n and π_n.

The paper studies automatic verification of liveness properties with probability 1 over parameterized programs that include probabilistic transitions, and proposes two novel approaches to the problem. The first approach is based on a Planner that occasionally determines the outcome of a finite sequence of “random”choices, while the other random choices are performed non-deterministically.Using a Planner, a probabilistic protocol can be treated just like a non-probabilistic one and verified as such. The second approach is based on γ-fairness, a notion of fairness that is sound and complete for verifying simple temporal properties (whose only temporal operators are ⋄and □) over finite-state systems.The paper presents a symbolic model checker based on γ-fairness.We then show how the network invariant approach can be adapted to accommodate probabilistic protocols. The utility of the Planner approach is demonstrated on a probabilistic mutual exclusion protocol. The utility of the approach of γ-fairness with network invariants is demonstrated on Lehman and Rabin's Courteous Philosophers algorithm.

We introduce a second-order polymorphic π-calculus based on duality principles. The calculus and its behavioural theories cleanly capture some of the core elements of significant technical development on polymorphic calculi in the past. This allows precise embedding of generic sequential functions as well as seamless integration with imperative constructs such as state and concurrency. Two behavioural theories are presented and studied, one based on a second-order logical relation and the other based on a polymorphic labelled transition system. The former gives a sound and complete characterisation of the contextual congruence, while the latter offers a tractable reasoning tool for a wide range of generic behaviours. The applicability of these theories is demonstrated through non-trivial reasoning examples and a fully abstract embedding of System F, the second-order polymorphic λ-calculus.

Lossy channel systems (LCS’s) are systems of finite state automata that communicate via unreliable unbounded fifo channels. We propose a new probabilistic model for these systems, where losses of messages are seen as faults occurring with some given probability, and where the internal behavior of the system remains nondeterministic, giving rise to a reactive Markov chains semantics. We then investigate the verification of linear-time properties on this new model.

Explicit substitutions (ES)were introduced as a bridge between the theory of rewrite systems with binders and substitution,such as the λ -calculus,and their implementation.In a seminal paper P.- A.Melliès observed that the dynamical properties of a rewrite system and its ES-based implementation may not coincide:he showed that a strongly normalising term (i.e. one which does not admit in finite derivations)in the λ -calculus may lose this status in its ES-based implementation.This paper studies normalisation for the latter systems in the general setting of higher-order rewriting:Based on recent work extending the theory of needed strategies to non-orthogonal rewrite systems we show that needed strategies normalise in the ES-based implementation of any orthogonal pattern higher-order rewrite system.

We investigate expressiveness of a fragment of the ambient calculus, a formalism for describing distributed and mobile computations. More precisely, we study expressiveness of the pure and public ambient calculus from which the capability open has been removed, in terms of the reachability problem of the reduction relation. Surprisingly, we show that even for this very restricted fragment, the reachability problem is not decidable. At a second step, for a slightly weaker reduction relation, we prove that reachability can be decided by reducing this problem to markings reachability for Petri nets. Finally, we show that the name-convergence problem as well as the model-checking problem turn out to be undecidable for both the original and the weaker reduction relation.

We provide several machine-independent characterizations of deterministic complexity classes in the model of computation proposed by L. Blum, M. Shub and S. Smale. We provide a characterization of partial recursive functions over any arbitrary structure. We show that polynomial time computable functions over any arbitrary structure can be characterized in term of safe recursive functions. We show that polynomial parallel time decision problems over any arbitrary structure can be characterized in terms of safe recursive functions with substitutions.

In previous work we have investigated a notion of approximate bisimilarity for labelled Markov processes. We argued that such a notion is more realistic and more feasible to compute than (exact) bisimilarity. The main technical tool used in the underlying theory was the Hutchinson metric on probability measures. This paper gives a more fundamental characterization of approximate bisimilarity in terms of the notion of (exact) similarity. In particular, we show that the topology of approximate bisimilarity is the Lawson topology with respect to the simulation preorder. To complement this abstract characterization we give a statistical account of similarity, and by extension, of approximate bisimilarity, in terms of the process testing formalism of Larsen and Skou.

We define an operational semantics and a type system for manipulating semistructured data that contains hidden information. The data model is simple labeled trees with a hiding operator. Data manipulation is based on patternmatching, with types that track the use of hidden labels.

Transition probabilities are proposed as the stochastic counterparts to set-based relations. We propose the construction of the converse of a stochastic relation. It is shown that two of the most useful properties carry over: the converse is idempotent as well as anticommutative. The nondeterminism associated with a stochastic relation is defined and briefly investigated. We define a bisimulation relation, and indicate conditions under which this relation is transitive; moreover it is shown that bisimulation and converse are compatible.

We develop a system of type assignment with intersection types, union types, indexed types, and universal and existential dependent types that is sound in a call-by-value functional language. The combination of logical and computational principles underlying our formulation naturally leads to the central idea of type-checking subterms in evaluation order. We thereby provide a uniform generalization and explanation of several earlier isolated systems. The proof of progress and type preservation, usually formulated for closed terms only, relies on a notion of definite substitution.

We define a cones and foci proof method, which rephrases the question whether two system specifications are branching bisimilar in terms of proof obligations on relations between data objects. Compared to the original cones and foci method from Groote and Springintveld [22], our method is more generally applicable, and does not require a preprocessing step to eliminate τ -loops. We prove soundness of our approach and give an application.

We prove that the satisfiability problem for the two-variable guarded fragment with transitive guards GF ²+TG 2EXPTIME-hard. This result closes the open questions left in [4],[17].In fact,we show 2EXPTIME-hardness of minGF ² +TG a fragment of GF ² +TG with- out equality and with just one transitive relation .,which is the only non-unary symbol allowed. Our lower bound for minGF ² +TG the upper bound for the whole guarded fragment with transitive guards and the unrestricted number of variables GF +TG by Szwast and Tendera [17 ],so in fact GF ²+TG 2EXPTIME-complete. It is surpris- ing that the complexity of minGF ² +TG higher then the complexity of the variant with one-way transitive guards GF ² +TG [9 ]. The latter logic appears naturally as a counterpart of temporal logics without past operators.

We present an analysis of the “linearly used continuationpassing interpretation” of functional languages, based on game semantics. This consists of a category of games with a coherence condition on moves —yielding a fully abstract model of an affine type-theory—and a syntax-independent and full embedding of a category of HO-style “wellbracketed” games into it. We show that this embedding corresponds precisely to linear CPS interpretation in its action on a games model of the call-by-value (untyped) λ-calculus, yielding a proof of full abstraction for the associated translation.

Multitree are unranked, unordered trees and occur in many Computer Science applications like rewriting and logic, knowledge representation, XML queries, typing for concurrent systems, cryptographic protocols.... We define constrained multitree automata which accept sets of multitrees where the constraints are expressed in a first-order theory of multisets with counting formulae which is very expressive and decidable. The resulting class of multitree automata is closed under boolean combination, has a decidable emptiness problem and we show that this class strictly embeds all previous classes of similar devices which have been defined for a whole variety of applications.

Circular assume-guarantee reasoning is used for the compositional verification of concurrent systems. Its soundness has been studied in depth, perhaps because circularity makes it anything but obvious. In this paper, we investigate completeness. We show that compositional circular assume-guarantee rules cannot be both sound and complete.

We describe a metalanguage MMML, which makes explicit the order of evaluation (in the spirit of monadic metalanguages) and the staging of computations (as in languages for multi-level bindingtime analysis). The main contribution of the paper is an operational semantics which is sufficiently detailed for analyzing subtle aspects of multi-stage programming, but also intuitive enough to serve as a reference semantics. For instance, the separation of computational types from code types, makes clear the distinction between a computation for generating code and the generated code, and provides a basis for multi-lingual extensions, where a variety of programming languages (aka monads) coexist. The operational semantics consists of two parts: local (semantics preserving) simpli.cation rules, and computation steps executed in a deterministic order (because they may have side-effects). We focus on the computational aspects, thus we adopt a simple type system, that can detect usual type errors, but not the unresolved link errors. Because of its explicit annotations, MMML is suitable as an intermediate language.

Combining Higher Order Abstract Syntax (HOAS) and (co)- induction is well known to be problematic. In previous work [1] we have described the implementation of a tool called Hybrid, within Isabelle HOL, which allows object logics to be represented using HOAS, and reasoned about using tactical theorem proving and principles of (co)induction. Moreover, it is definitional, which guarantees consistency within a classical type theory. In this paper we describe how to use it in a multi-level reasoning fashion, similar in spirit to other meta-logics such FOλ△^IN and Twelf. By explicitly referencing provability, we solve the problem of reasoning by (co)induction in presence of non-stratifiable hypothetical judgments, which allow very elegant and succinct specifications. We demonstrate the method by formally verifying the correctness of a compiler for (a fragment) of Mini-ML, following [10]. To further exhibit the flexibility of our system, we modify the target language with a notion of non-well-founded closure, inspired by Milner & Tofte [16] and formally verify via co-induction a subject reduction theorem for this modified language.

G-relative pushouts (GRPOs) have recently been proposed by the authors as a new foundation for Leifer and Milner's approach to deriving labelled bisimulation congruences from reduction systems. This paper develops the theory of GRPOs further, arguing that they provide a simple and powerful basis towards a comprehensive solution. As an example, we construct GRPOs in a category of ‘nches and wirings.’ then examine the approach based on Milner's precategories and Leifer's functorial reactive systems, and show that it can be recast in a much simpler way into the 2-categorical theory of GRPOs.

In this paper we study induction in the context of the firstorder μ-calculus with explicit approximations. We present and compare two Gentzen-style proof systems each using a different type of induction. The first is based on finite proof trees and uses a local well-founded induction rule, while the second is based on (finitely represented) ω-regular proof trees and uses a global induction discharge condition to ensure externally that all inductive reasoning is well-founded. We give effective procedures for the translation of proofs between the two systems, thus establishing their equivalence.