We define a Public Announcement Separation Logic (PASL) that allows us to consider epistemic possible worlds as resources that can be shared or separated, in the spirit of separation logics. After studying its semantics and illustrating its interest for modelling systems, we provide a sound and complete tableau calculus that deals with resource, agent and announcement constraints and give also a countermodel extraction method.

Perturbation theory has always been an important component of the natural sciences. From celestial mechanics to the quantum theory of fields, it has always played a central role, which this little note sets out to analyse briefly. We will show, in particular, how its epistemological position has changed from being just a ‘tool’ to being the basis of definition for objects in quantum field theory.

Proofs with logical relations play a key role to establish rich properties such as normalization or contextual equivalence. They are also challenging to mechanize. In this paper, we describe two case studies using the proof environment Beluga: First, we explain the mechanization of the weak normalization proof for the simply typed lambda-calculus; second, we outline how to mechanize the completeness proof of algorithmic equality for simply typed lambda-terms where we reason about logically equivalent terms. The development of these proofs in Beluga relies on three key ingredients: (1) we encode lambda-terms together with their typing rules, operational semantics, algorithmic and declarative equality using higher order abstract syntax (HOAS) thereby avoiding the need to manipulate and deal with binders, renaming and substitutions, (2) we take advantage of Beluga's support for representing derivations that depend on assumptions and first-class contexts to directly state inductive properties such as logical relations and inductive proofs, (3) we exploit Beluga's rich equational theory for simultaneous substitutions; as a consequence, users do not need to establish and subsequently use substitution properties, and proofs are not cluttered with references to them. We believe these examples demonstrate that Beluga provides the right level of abstractions and primitives to mechanize challenging proofs using HOAS encodings. It also may serve as a valuable benchmark for other proof environments.

In this short note we study the semantics of two basic computational effects, exceptions and states, from a new point of view. In the handling of exceptions we dissociate the control from the elementary operation that recovers from the exception. In this way it becomes apparent that there is a duality, in the categorical sense, between exceptions and states.

In Girard (2001), J.-Y. Girard presents a new theory, The Ludics, which is a model of realisibility of logic that associates proofs with designs, and formulas with behaviours. In this article we study the interpretation in this semantics of formulas with first-order quantifications and their proofs. We extend to the first-order quantifiers the full completeness theorem obtained in Girard (2001) for $MALL_2$. A significant part of this article is devoted to the study of a uniformity property for the families of designs that represent proofs of formulas depending on a first-order free variable.

Simply typed λ-calculus with fixpoint combinators, λY-calculus, offers an interesting method for approximating program semantics. The Böhm tree of a λY-term represents the meaning of the program up to the meaning of built-in constants. It is much easier to reason about properties of such trees than properties of interpreted programs. Moreover, some interesting properties of programs are already expressible on the level of these trees.

Collapsible pushdown automata (CPDA) give another way of generating the same class of trees as λY-terms. We clarify the relationship between the two models. In particular, we present two relatively simple translations from λY-terms to CPDA using Krivine machines as an intermediate step. The latter are general machines for describing computation of the weak head normal form in the λ-calculus. They provide the notions of closure and environment that facilitate reasoning about computation.

Least fixpoints are constructed for finite coproducts of definable endofunctors of Cartesian closed categories that have weak polynomial products and joint equalizers of arbitrary families of pairs of parallel arrows. Both conditions hold in PER, the category whose objects are partial equivalence relations on N, and whose arrows are partial recursive functions. Weak polynomial products exist in any cartesian closed category with a finite number of objects as well as in any model of second order polymorphic lambda calculus: that is, in the proof theory of any second order positive intuitionistic propositional calculus, but such a category need not have equalizers. However, any finite coproduct of definable endofunctors of a cartesian closed category with weak polynomial products will have a least fixpoint in a larger category with equalizers whose objects are right ideals (or sieves) of modulo certain congruence relations, and whose arrows are induced from .

$\mathcal{M}$-adhesive categories provide an abstract framework for a large variety of specification frameworks for modelling distributed and concurrent systems. They extend the well-known frameworks of adhesive and weak adhesive HLR categories and integrate high-level constructs such as attribution as in the case of typed attributed graphs.

In the current paper, we investigate $\mathcal{M}$-adhesive transformation systems including negative application conditions (NACs) for transformation rules, which are often used in applications. For such systems, we propose an original equivalence on transformation sequences, called permutation equivalence, that is coarser than the classical switch equivalence. We also present a general construction of deterministic processes for $\mathcal{M}$-adhesive transformation systems based on subobject transformation systems. As a main result, we show that the process obtained from a transformation sequence identifies its equivalence class of permutation-equivalent transformation sequences. Moreover, we show how the analysis of this process can be reduced to the analysis of the reachability graph of a generated Place/Transition Petri net. This net encodes the dependencies between rule applications of the transformation sequence, including the inhibiting effects of the NACs.

We present a dependent-type system for a λ-calculus with explicit substitutions. In this system, meta-variables, as well as substitutions, are first-class objects. We show that the system enjoys properties like type uniqueness, subject reduction, soundness, confluence, and weak normalization.

The study of algebraic modelling of labelled non-deterministic concurrent processes leads us to consider a category LB, obtained from a complete meet-semilattice B and from B-valued equivalence relations. We prove that, if B has enough properties, then LB presents a two-fold internal logical structure, induced by two doctrines definable on it: one related to its families of subobjects and one to its families of regular subobjects. The first doctrine is Heyting and makes LB a Heyting category, the second one is Boolean. We will see that the difference between these two logical structures, namely the different behaviour of the negation operator, can be interpreted in terms of a distinction between non-deterministic and deterministic behaviours of agents able to perform computations in the context of the same process. Moreover, the sorted first-order logic naturally associated with LB can be extended to a modal/temporal logic, again using the doctrinal setting. Relations are also drawn to other computational models.

We extend the proof-irrelevant model defined in Smith (1988) to the whole of Martin-Löf's logical framework. The main difference here is the existence of a type whose objects themselves represent types rather than proof-objects. This means that the model must now be able to distinguish between objects with different degree of relevance: those that denote proofs are irrelevant whereas those that denote types are not. In fact a whole hierarchy of relevance exists.

Another difference is the higher level of detail in the formulation of the formal theory, such as the explicit manipulation of contexts and substitutions. This demands an equally detailed definition of the model, including interpreting contexts and substitutions.

We are thus led to a whole reformulation of the proof-irrelevant model. We present a model that is built up from an arbitrary model of the untyped lambda calculus. We also show how to extend it when the logical framework itself is enlarged with inductive definitions. In doing so, a variant of Church numerals is introduced.

As in Smith (1988), the model can only be defined in the absence of universes, and it is useful to obtain an elementary proof of consistency and to prove the independence of Peano's fourth axiom.

The languages accepted by finite automata are precisely the languages denoted by regular expressions. In contrast, finite automata may exhibit behaviours that cannot be described by regular expressions up to bisimilarity. In this paper, we consider extensions of the theory of regular expressions with various forms of parallel composition and study the effect on expressiveness. First we prove that adding pure interleaving to the theory of regular expressions strictly increases its expressiveness modulo bisimilarity. Then, we prove that replacing the operation for pure interleaving by ACP-style parallel composition gives a further increase in expressiveness, still insufficient, however, to facilitate the expression of all finite automata up to bisimilarity. Finally, we prove that the theory of regular expressions with ACP-style parallel composition and encapsulation is expressive enough to express all finite automata up to bisimilarity. Our results extend the expressiveness results obtained by Bergstra, Bethke and Ponse for process algebras with (the binary variant of) Kleene's star operation.

Final coalgebras capture system behaviours such as streams, infinite trees and processes. Algebraic operations on a final coalgebra can be defined by distributive laws (of a syntax functor Σ over a behaviour functor F). Such distributive laws correspond to abstract specification formats. One such format is a generalisation of the GSOS rules known from structural operational semantics of processes. We show that given an abstract GSOS specification ρ that defines operations σ on a final F-coalgebra, we can systematically construct a GSOS specification ρ that defines the pointwise extension σ of σ on a final FA-coalgebra. The construction relies on the addition of a family of auxiliary ‘buffer’ operations to the syntax. These buffer operations depend only on A, so the construction is uniform for all σ and F.

We give a definition of Q-net, a generalization of Petri nets based on a Lawvere theory Q, for which many existing variants of Petri nets are a special case. This definition is functorial with respect to change in Lawvere theory, and we exploit this to explore the relationships between different kinds of Q-nets. To justify our definition of Q-net, we construct a family of adjunctions for each Lawvere theory explicating the way in which Q-nets present free models of Q in Cat. This gives a functorial description of the operational semantics for an arbitrary category of Q-nets. We show how this can be used to construct the semantics for Petri nets, pre-nets, integer nets, and elementary net systems.

The uniform word problem for finitely presented ortholattices is shown to be solvable through a method of terminating proof search. The axioms of ortholattices are all Harrop formulas, and thus can be expressed in natural deduction style as single succedent rules. A system of natural deduction style rules for orthologic is given as an extension of the system for lattices presented by Negri and von Plato. By considering formal derivations of atomic formulas from a finite number of given atomic formulas, it is shown that proof search is bounded, and thus that the question of derivability of any atomic formula from any finite set of given atomic formulas is decidable.

The symmetric interaction combinators are a variant of Lafont's interaction combinators. They enjoy a weaker universality property with respect to interaction nets, but are equally expressive. They are a model of deterministic distributed computation and share the good properties of Turing machines (elementary reductions) and of the λ-calculus (higher-order functions and parallel execution). We introduce a denotational semantics for this system, which is inspired by the relational semantics for linear logic, and prove an injectivity and full completeness result for it. We also consider the algebraic semantics defined by Lafont, and prove that the two are strongly related.

We define a constructive model for ${\Delta^0_2}$-maps, that is, maps recursively definable from a map deciding the halting problem. Our model refines an existing constructive interpretation for classical reasoning over one-quantifier formulas: it is compositional (Modus Ponens is interpreted as an application) and semantical (rather than translating classical proofs into intuitionistic ones, we define a mathematical structure intuitionistically validating excluded middle for one-quantifier formulas).

In a recent paper, Girard (2012) proposed to use his recent construction of a geometry of interaction in the hyperfinite factor (Girard 2011) in an innovative way to characterize complexity classes. We begin by giving a detailed explanation of both the choices and the motivations of Girard's definitions. We then provide a complete proof that the complexity class co-NL can be characterized using this new approach. We introduce the non-deterministic pointer machine as a technical tool, a concrete model to compute algorithms.

A well-known result by Palamidessi tells us that πmix (the π-calculus with mixed choice) is more expressive than πsep (its subset with only separate choice). The proof of this result analyses their different expressive power concerning leader election in symmetric networks. Later on, Gorla offered an arguably simpler proof that, instead of leader election in symmetric networks, employed the reducibility of ‘incestual’ processes (mixed choices that include both enabled senders and receivers for the same channel) when running two copies in parallel. In both proofs, the role of breaking (initial) symmetries is more or less apparent. In this paper, we shed more light on this role by re-proving the above result – based on a proper formalization of what it means to break symmetries – without referring to another problem domain like leader election.

Both Palamidessi and Gorla rephrased their results by stating that there is no uniform and reasonable encoding from πmix into πsep. We indicate how their proofs can be adapted and exhibit the consequences of varying notions of uniformity and reasonableness. In each case, the ability to break initial symmetries turns out to be essential. Moreover, by abandoning the uniformity criterion, we show that there indeed is a reasonable encoding. We emphasize its underlying principle, which highlights the difference between breaking symmetries locally instead of globally.

We show that there is a computably enumerable function f (that is, computably approximable from below) that dominates almost all functions, and f ⊕ W is incomplete for all incomplete computably enumerable sets W. Our main methodology is the LR equivalence relation on reals: A ≡LRB if and only if the notions of A-randomness and B-randomness coincide. We also show that there are c.e. sets that cannot be split into two c.e. sets of the same LR degree. Moreover, a c.e. set is low for random if and only if it computes no c.e. set with this property.