Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL

Refutation of Sallé's Longstanding Conjecture

In a recent work, Breuvart et al. have shown that Morris's theory satisfies the omega-rule. In this paper we demonstrate that the two aforementioned theories actually coincide, thus disproving Sallé's conjecture.

Models of Type Theory Based on Moore Paths

Confluence of an extension of Combinatory Logic by Boolean constants.

A sequent calculus for semi-associativity

Generalized Refocusing: from Hybrid Strategies to Abstract Machines

Combinatorial Flows and their Normalisation

List Objects with Algebraic Structure

Streett Automata Model Checking of Higher-Order Recursion Schemes

Polynomial running times for polynomial-time oracle machines

The Complexity of Principal Inhabitation

Optimality and the Linear Substitution Calculus

Types as Resources for Classical Natural Deduction

Displayed categories

A displayed category over a category C is equivalent to "a category D and functor F : D -> C", but instead of having a single collection of "objects of D" with a map to the objects of C, the objects are given as a family indexed by objects of C, and similarly for the morphisms. This encapsulates a common way of building categories in practice, by starting with an existing category and adding extra data/properties to the objects and morphisms.

The interest of this seemingly trivial reformulation is that various properties of functors are more naturally defined as properties of the corresponding displayed categories. Fibrations, for example, when defined as certain functors, use equality on objects in their definition. When defined instead as a property of displayed categories, no reference to equality on objects is required. Moreover, almost all examples of fibrations in nature are, in fact, categories whose standard construction can be seen as going via displayed categories.

We therefore propose displayed categories as a basis for the development of fibrations in the type-theoretic setting, and similarly for various other notions whose classical definitions involve equality on objects.

Besides giving a conceptual clarification of such issues, displayed categories also provide a powerful tool in computer-formalisation, unifying and abstracting common constructions and proof-techniques of category theory. As such, most of the material of this article has been formalised in Coq over the UniMath library, with the aim of providing a practical library for use in further developments.

The confluent terminating context-free substitutive rewriting system for the lambda-calculus with surjective pairing and terminal type

A Curry-Howard Approach to Church’s Synthesis

Observably Deterministic Concurrent Strategies and Intensional Full Abstraction for Parallel-or

Is the optimal implementation inefficient? Elementarily not

A polynomial-time algorithm for the Lambek calculus with brackets of bounded order

Dinaturality between syntax and semantics

Arrays and References in Resource Aware ML

Böhm Reduction in Infinitary Term Graph Rewriting Systems

Relating System F and $\lambda$2: A Case Study in Coq, Abella and Beluga

Infinite Runs in Abstract Completion

There is only one notion of differentiation

This suggests the view that there is only one notion of differentiation but, as one varies the setting, it admits rather different presentations.

Improving Rewriting Induction Approach for Proving Ground Confluence

A Fibrational Framework for Substructural and Modal Logics

In this paper, we define a general framework that abstracts the common features of many intuitionistic substructural and modal logics. The framework is a sequent calculus / normal-form type theory parametrized by a _mode theory_, which is used to describe the structure of contexts and the structural properties they obey. The framework makes use of resource annotations, where we pair the context itself, which obeys standard structural properties, with a term, drawn from the mode theory, that constrains how the context can be used. Product types, implications, and modalities are defined as instances of two general connectives, one positive and one negative, that manipulate these resource annotations. We show that specific mode theories can express non-associative, ordered, linear, affine, relevant, and cartesian products and implications; monoidal and non-monoidal comonads and adjunctions; strong and non-strong monads; n-linear variables; bunched implications; and the adjunctions that arose in our work on homotopy type theory. We prove cut (and identity) admissibility independently of the mode theory, obtaining it for all of the above logics at once. Further, we give a general equational theory on derivations / terms that, in addition to the usual beta-eta rules, characterizes when two derivations differ only by the placement of structural rules. Finally, we give an equivalent semantic presentation of these ideas, in which a mode theory corresponds to a 2-dimensional cartesian multicategory, and the framework corresponds to another such multicategory with a functor to the mode theory. The logical connectives have universal properties relative to this functor, making it into a bifibration. The sequent calculus rules and the equational theory on derivations are sound and complete for this. The resulting framework can be used both to understand existing logics / type theories and to design new ones.

Negative Translations and Normal Modality

Continuation Passing Style for Effect Handlers

We refine the initial CPS translation first by uncurrying it to yield a properly tail-recursive translation and second by making it higher-order in order to contract administrative redexes at translation time. We prove that the higher-order CPS translation simulates effect handler reduction. We have implemented the higher-order CPS translation as a backend for the Links web programming language.