We investigate cut elimination in propositional substructural logics. The problem is to decide whether a given calculus admits (reductive) cut elimination. We show that for commutative single-conclusion sequent calculi containing generalised knotted structural rules and arbitrary logical rules the problem can be decided by resolution-based methods. A general cut-elimination proof for these calculi is also provided.

The context of this article is the programme to develop monoidal bicategories with a feedback operation as an algebra of processes, with applications to concurrency theory. The objective here is to study reachability, minimization and minimal realization in these bicategories. In this setting the automata are 1-cells, in contrast with previous studies where they appeared as objects. As a consequence, we are able to study the relation of minimization and minimal realization to serial composition of automata using (co)lax (co)monads. We are led to define suitable behaviour categories and prove minimal realization theorems that extend classical results.

We give a negative answer to the question of whether every partial combinatory algebra can be completed. The explicit counterexample will be an intricately constructed term model. The construction and the proof that it works depend heavily on syntactic techniques. In particular, it provides a nice example of reasoning with elementary diagrams and descendants. We also include a domain-theoretic proof of the existence of an incompletable partial combinatory algebra.

We present an interdisciplinary effort in the field of global environmental change, related to the understanding of the concept of ‘vulnerability’. We have used functional programming to capture the generic aspects of the myriad of definitions of vulnerability, and have used the resulting formalization to learn something new about vulnerability and to write some better software for vulnerability assessment. In the process, we have also found out something about formalization in general, about the advantages and disadvantages of dependent types, and about the role of computing science in the larger intellectual landscape.

In this paper, we describe three distinct monoids over domains, each with a commutative analog, which define bag domain monoids. Our results were inspired by work by Varacca (Varacca 2003), and they lead to a constructive approach to his Hoare indexed valuations over a continuous poset $P$. We use our constructive approach to describe an analog of the probabilistic power domain, and the laws that characterise it, that forms a Scott-closed subset of Varacca's construct. We call these the Hoare random variables over$P$.

Using the concept of a generalised priority constraint satisfaction problem, we previously found a way to introduce priority queries into fuzzy relational databases. The results were PFSQL (Priority Fuzzy Structured Query Language) together with a database independent interpreter for it. In an effort to improve the performance of the resolution of PFSQL queries, the aim of the current paper is to formalise PFSQL queries by obtaining their interpretation in an existing fuzzy logic. We have found that the ŁΠ logic provides sufficient elements. The SELECT line of PFSQL queries is semantically a formula of some fuzzy logic, and we show that such formulas can be naturally expressed in a conservative extension of the ŁΠ logic. Furthermore, we prove a theorem that gives the PSPACE containment for the complexity of finding a model for a given ŁΠ logic formula.

On December 5, 1997, a small conference was held at McGill on the occasion of Jim Lambek's 75th birthday. Subsequently it was decided to publish two volumes of papers contributed in his honour to mark this occasion: this issue of Mathematical Structures in Computer Science is one of the volumes; the other is Volume 6 of the journal Theory and Applications of Categories. At the December 1997 conference, a brief biographical essay was presented by Michael Barr and appears in the TAC volume. However, we wish to make some further remarks here.

Jim completed his Ph.D. at McGill under Hans Zassenhaus in 1950, and has remained at McGill since then. But it is of interest to note that Jim wrote two theses: the second involved biquaternions in mathematical physics, and so foreshadows a significant feature of his career: Jim has consistently shown a remarkable range of interests, from physics to linguistics, from algebra to logic, from the history and philosophy of mathematics to the theory of computing science (although he never touches a computer, to this day!). Let us just review a small sample of his more than 100 published papers.

This article explores methods to provide computer support for reasoning about graph transformations. We first define a general framework for representing graphs, graph morphisms and single graph rewriting steps. This setup allows for interactively reasoning about graph transformations. In order to achieve a higher degree of automation, we identify fragments of the graph description language in which we can reduce reasoning about global graph properties to reasoning about local properties, involving only a bounded number of nodes, which can be decided by Boolean satisfiability solving or even by deterministic computation of low complexity.

We define an extension of pure type systems with explicit substitution. We show that the type systems with explicit substitution are strongly normalizing iff their ordinary counterparts are. Subject reduction is shown to fail in general but a weaker, though still useful, subject reduction property is established. A more complicated extension is proposed for which subject reduction does hold in general.

Certain ‘Finite Structure Conditions’ on a geometric theory are shown to be sufficient for its classifying topos to be a presheaf topos. The conditions assert that every homomorphism from a finite structure of the theory to a model factors via a finite model, and they hold in cases where the finitely presentable models are all finite.

The conditions are shown to hold for the theory of strongly algebraic (or SFP) information systems and some variants, as well as for some other theories already known to be classified by presheaf toposes.

The work adheres to geometric constructivism throughout, and in consequence provides ‘topical’ categories of domains (internal in the category of toposes and geometric morphisms) with an analogue of Plotkin's double characterization of strongly algebraic domains, by sets of minimal upper bounds and by sequences of finite posets.

In this paper, we propose a new and elegant definition of the class of recursive functions, which is analogous to Kleene's definition but differs in the primitives taken, thus demonstrating the computational power of the concurrent programming language introduced in Walters (1991), Walters (1992) and Khalil and Walters (1993).

The definition can be immediately rephrased for any distributive graph in a countably extensive category with products, thus allowing a wide, natural generalization of computable functions.

Is the current formulation of multiset theory, which is based on sets and multiplicities of their elements, adequate? We exhibit both mathematical and metamathematical reasons which should cause one to rethink the definition. Some problems with multiset theory in its accepted formulation concern even the basic operations of union, intersection, and complement; others, more deeply rooted, concern Cartesian products, relations, or morphisms. We compare current definitions and conclude that the problems of multiset theory need to be resolved at the fundamental level of sets and mappings (or equivalent constructs) with multiplicities introduced only as a secondary concept. As a consequence, we propose to define multisets as families. A mapping establishes the connection to the familiar theory of multisets. Without losing anything, our proposal is simple and provides for an elegant mathematical theory.

Weakest precondition transformers are useful tools in program verification. One of their key properties is composability, that is, the weakest precondition predicate transformer (wppt for short) associated to program $f;\;g$ should be equal to the composition of the wppts associated to f and g. In this paper, we study the categorical structure behind wppts from a fibrational point of view. We characterize the wppts that satisfy composability as the ones constructed from the Cartesian lifting of a monad. We moreover show that Cartesian liftings of monads along lax slice categories bijectively correspond to Eilenberg–Moore monotone algebras. We then instantiate our techniques by deriving wppts for commonplace effects such as the maybe monad, the nonempty powerset monad, the counter monad, or the distribution monad. We also show how to combine them to derive the wppts appearing in the literature of verification of probabilistic programs.

We present a categorical model for intuitionistic linear logic in which objects are polynomial diagrams and morphisms are simulation diagrams. The multiplicative structure (tensor product and its adjoint) can be defined in any locally cartesian closed category, but the additive (product and coproduct) and exponential (-comonoid comonad) structures require additional properties and are only developed in the category Set, where the objects and morphisms have natural interpretations in terms of games, simulation and strategies.

We prove a full completeness theorem for MLL without the Mix rule. This is done by interpreting a proof as a dinatural transformation in a *-autonomous category of reflexive topological abelian groups first studied by Barr, denoted [Rscr ][Tscr ][Ascr ]. In Section 2, we prove the unique interpretation theorem for a binary provable MLL-sequent. In Section 3, we prove a completeness theorem for binary sequents in MLL without the Mix rule, where we interpret formulas in the category [Rscr ][Tscr ][Ascr ]. The theorem is proved by investigating the concrete structure of [Rscr ][Tscr ][Ascr ], especially that arising from Pontrjagin's work on duality.

A Gentzen sequent calculus for Lax Logic is presented, the proofs in which correspond naturally in a 1–1 way to the normal natural deductions for the logic. The propositional fragment of this calculus is used as the basis for another calculus that uses a history mechanism in order to give a decision procedure for propositional Lax Logic.

N. G. de Bruijn, now professor emeritus of the Eindhoven University of Technology, was a pioneer in the field of interactive theorem proving. From 1967 to the end of the 1970's, his work on the Automath system introduced the architecture that is common to most of today's proof assistants, and much of the basic technology. But de Bruijn was a mathematician first and foremost, as evidenced by the many mathematical notions and results that bear his name, among them de Bruijn sequences, de Bruijn graphs, the de Bruijn–Newman constant, and the de Bruijn–Erdös theorem. The quotation above is thus interesting not because it is a reflection on his expertise in formal verification, but, rather, of his convictions as a working mathematician.

We present a new model of guarded dependent type theory (GDTT), a type theory with guarded recursion and multiple clocks in which one can program with and reason about coinductive types. Productivity of recursively defined coinductive programs and proofs is encoded in types using guarded recursion and can therefore be checked modularly, unlike the syntactic checks implemented in modern proof assistants. The model is based on a category of covariant presheaves over a category of time objects, and quantification over clocks is modelled using a presheaf of clocks. To model the clock irrelevance axiom, crucial for programming with coinductive types, types must be interpreted as presheaves internally right orthogonal to the object of clocks. In the case of dependent types, this translates to a lifting condition similar to the one found in homotopy theoretic models of type theory, but here with an additional requirement of uniqueness of lifts. Since the universes defined by the standard Hofmann–Streicher construction in this model do not satisfy this property, the universes in GDTT must be indexed by contexts of clock variables. We show how to model these universes in such a way that inclusions of clock contexts give rise to inclusions of universes commuting with type operations on the nose.

The aim of the research domain known as process mining is to use process discovery to construct a process model as an abstract representation of event logs. The goal is to build a model (in terms of a Petri net) that can reproduce the logs under consideration, and does not allow different behaviours compared with those shown in the logs. In particular, process mining aims to verify the accuracy of the model design (represented as a Petri net), basically checking whether the same net can be rediscovered. However, the main mining methods proposed in the literature have some drawbacks: the classical α-algorithm is unable to rediscover various nets, while the region-based approach, which can mine them correctly, is too complex.

In this paper, we compare different approaches and propose some ideas to counter the weaknesses of the region-based approach.

Recently, encodings in interaction nets of the call-by-name and call-by-value strategies of the $\lambda$-calculus have been proposed. The purpose of these encodings is to bridge the gap between interaction nets and traditional abstract machines, which are both used to provide lower-level specifications of strategies of the $\lambda$-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 evaluation flow. Another benefit of this approach is that no artifact is needed to represent boxes. However, these encodings deliberately follow the implemented strategies (call-by-name and call-by-value) as closely as possible, and hence do not benefit from the ability of interaction nets to represent sharing easily. The aim of this paper is to show that better sharing (hence efficiency) can indeed be achieved without adding much structure. We thus present the call-by-need strategy following the same philosophy, which is, indeed, no more complicated than call-by-name. We also extend our approach to fully lazy reduction. 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 $\lambda$-calculus.