Bi-inductive Structural Semantics: (Extended Abstract)

We propose a simple order-theoretic generalization of set-theoretic inductive definitions. This generalization covers inductive, co-inductive and bi-inductive definitions and is preserved by abstraction. This allows the structural operational semantics to describe simultaneously the finite/terminating and infinite/diverging behaviors of programs. This is illustrated on the structural bifinitary small/big-step trace/relational/operational semantics of the call-by-value λ-calculus.     

A Calculus for Reconfiguration: (Extended abstract)

We present a simple calculus, called R-calculus (for “reconfiguration”), intended to provide a kernel model for a computational paradigm in which standard execution (that is, execution of a single computation described by a fragment of code) can be interleaved with operations at the meta-level which can manipulate in various ways the context in which this computation takes place. Formally, this is achieved by introducing as basic terms of the calculus configurations, which are, roughly speaking, pairs consisting of an (open, mutually recursive) collection of named components and a term representing a program running in the context of these components. The R-calculus has been originally developed as a formal model for programming-in-the large, where computations correspond to applications running in some context of software components, and operations at the meta-level correspond to the possibility of dynamically loading, updating or in general manipulat- ing these software components without stopping the application. However, the calculus can also encode programming-in-the-small issues, because configurations combine the features of lambda- abstractions (first-class functions), records, environments with mutually recursive definitions, and modules. We state confluence of the calculus and define a call-by-need strategy which leads to a generalization, including reconfiguration features, of call-by-need lambda-calculi.     

Simulations Up-to and Canonical Preorders: (Extended Abstract)

In this paper we define simulations up-to a preorder and show how we can use them to provide a coinductive, simulation-like, characterization of semantic preorders for processes. The result applies to a wide class of preorders, in particular to all semantic preorders coarser than the ready simulation preorder in the linear time-branching time spectrum. An interesting but unexpected result is that, when built from an equivalence relation, the simulation up-to is a canonical preorder whose kernel is the given equivalence relation. These canonical preorders have several nice properties, the main being that since all of them are defined in a homogeneous way, their properties can be proved in a generic way. In particular, we present an axiomatic characterization of each of these canonical preorders, that is obtained just by adding a single axiom to the axiomatization of the original equivalence relation. This gives us an alternative axiomatization for every axiomatizable preorder in the linear time-branching time spectrum, whose correctness and completeness can be proved once and for all.     

Nominal Reasoning Techniques in Coq: (Extended Abstract)

We explore an axiomatized nominal approach to variable binding in Coq, using an untyped lambda-calculus as our test case. In our nominal approach, alpha-equality of lambda terms coincides with Coq's built-in equality. Our axiomatization includes a nominal induction principle and functions for calculating free variables and substitution. These axioms are collected in a module signature and proved sound using locally nameless terms as the underlying representation. Our experience so far suggests that it is feasible to work from such axiomatized theories in Coq and that the nominal style of variable binding corresponds closely with paper proofs. We are currently working on proving the soundness of a primitive recursion combinator and developing a method of generating these axioms and their proof of soundness from a grammar describing the syntax of terms and binding.     

Local Bigraphs and Confluence: Two Conjectures: (Extended Abstract)

The notion of confluence is studied on the context of bigraphs. Confluence will be important in modelling real-world systems, both natural (as in biology) and artificial (as in pervasive computing). The paper uses bigraphs in which names have multiple locality; this enables a formulation of the lambda calculus with explicit substitutions. The paper reports work in progress, seeking conditions on a bigraphical reactive system that are sufficient to ensure confluence; the conditions must deal with the way that bigraphical redexes can be intricately intertwined. The conditions should also be satisfied by the lambda calculus. After discussion of these issues, two conjectures are put forward.     

Samuel Guttenplan,ed., A Companion to the Philosophy of Mind

Minds and Machines -     

A List-machine Benchmark for Mechanized Metatheory: (Extended Abstract)

We propose a benchmark to compare theorem-proving systems on their ability to express proofs of compiler correctness. In contrast to the first POPLmark, we emphasize the connection of proofs to compiler implementations, and we point out that much can be done without binders or alpha-conversion. We propose specific criteria for evaluating the utility of mechanized metatheory systems; we have constructed solutions in both Coq and Twelf metatheory, and we draw conclusions about those two systems in particular.     

Coinductive Counting: Bisimulation in Enumerative Combinatorics (Extended Abstract)

The recently developed coinductive calculus of streams finds here a further application in enumerative combinatorics. A general methodology is developed to solve a wide variety of basic counting problems in a uniform way: (1) the objects to be counted are enumerated by means of an infinite (weighted) automaton; (2) the automaton is minimized by means of the quantitative notion of stream bisimulation; (3) the minimized automaton is used to compute an expression (in terms of stream constants and operators) that represents the stream of all counts.     

Equivalences for Silent Transitions in Probabilistic Systems: (Extended Abstract)

We address abstraction in the setting of probabilistic reactive systems, and study its formal underpinnings for the strictly alternating model. In particular, we define the notion of branching bisimilarity and study its properties by studying two other equivalence relations, viz. coloured trace equivalence and branching bisimilarity using maximal probabilities. We show that both alternatives coincide with branching bisimilarity. The alternative characterisations have their own merits and focus on different aspects of branching bisimilarity. Together they give a better understanding of branching bisimilarity. A crucial observation, and, in fact a major motivation for this work is that the notions of branching bisimilarity in the alternating and in the non-alternating model differ, and that the latter one discriminates between systems that are intuitively branching bisimilar.