ABSTRACT. Higher-order beta-matching is the following decision problem: given two simply typed lambda-terms, can the first term be instantiated to be beta-equivalent to the second term? This problem was formulated by Huet in the 1970s and shown undecidable by Loader in 2003 by reduction from lambda-definability.

The present work provides a novel undecidability proof for higher-order beta-matching, in an effort to verify this result by means of a proof assistant in full detail. Rather than starting from lambda-definability, the presented proof encodes a restricted form of string rewriting as higher-order beta-matching. The particular approach is similar to Urzyczyn's undecidability result for intersection type inhabitation.

The presented approach has several advantages. First, the proof is simpler to verify in full detail due to the simple form of rewriting systems, which serve as a starting point. Second, undecidability of the considered problem in string rewriting is already certified using the Coq proof assistant. As a consequence, we obtain a certified many-one reduction from the Halting Problem to higher-order beta-matching. Third, the presented approach identifies a uniform construction which shows undecidability of higher-order beta-matching, lambda-definability, and intersection type inhabitation.

The presented undecidability proof is mechanized in the Coq proof assistant and contributed to the existing Coq Library of Undecidability Proofs.

ABSTRACT. We are looking at the generalization problem modulo some equational theories. This problem is dual to the unification problem: given two input terms, we want to find a common term whose respective two instances are equivalent to the original terms modulo the theory.

There exist algorithms for finding generalizations over various equational theories. Our focus is on modular construction of equational generalization algorithms for the union of signature-disjoint theories. Specifically, we consider the class of regular and collapse-free theories, showing how to combine existing generalization algorithms to produce specific solutions in these cases.

Additionally, we identify a class of theories that admit a generalization algorithm based on the application of axioms to resolve the problem. To define this class, we rely on the notion of syntactic theories, a concept originally introduced to develop unification procedures similar to the one known for syntactic unification. We demonstrate that syntactic theories are also helpful in developing generalization procedures that are similar to those used for syntactic generalization.

ABSTRACT. The unification type of an equational theory is defined using a preorder on substitutions, called the instantiation preorder, whose scope is either restricted to the variables occurring in the unification problem, or unrestricted such that all variables are considered. It has been known for more than three decades that the unification type of an equational theory may vary, depending on which instantiation preorder is used. More precisely, it was shown in 1991 that the theory ACUI of an associative, commutative, and idempotent binary function symbol with a unit is unitary w.r.t. the restricted instantiation preorder, but not unitary w.r.t. the unrestricted one. In 2016 this result was strengthened by showing that the unrestricted type of this theory also cannot be finitary. Here, we considerably improve on this result by proving that ACUI is infinitary w.r.t. the unrestricted instantiation preorder, thus precluding type zero. We also show that, w.r.t. this preorder, the unification type of ACU (where idempotency is removed from the axioms) and of AC (where additionally the unit is removed) is infinitary, though it is respectively unitary and finitary in the restricted case. In the other direction, we prove (using the example of unification in the description logic EL) that the unification type may actually improve from type zero to infinitary when switching from the restricted instantiation preorder to the unrestricted one. In addition, we establish some general results on the relationship between the two instantiation preorders.

ABSTRACT. The research area of cryptographic protocol analysis contains a number of innovative algorithms and procedures for checking various security properties of protocols. These procedures consider protocols modeled in a symbolic way, typically via a rewrite system or an equational theory. Most of these procedures focus on solving one of several knowledge problems that model intruder knowledge. Solving these problems can demonstrate the ability of the intruder to obtain some forbidden knowledge of the protocol, such as secret keys. Two important examples of these problems are the deduction problem and the static equivalence problem.

Deduction is concerned with the ability to derive a term from a set of terms (or knowledge) obtained from the observation of a protocol instance. Static equivalence, on the other hand, is concerned with distinguishing between two runs of a protocol based on two sets of knowledge. These two ``knowledge problems'' at first inspection appear to be very close to the older automated reasoning problems of matching and unification. However, this first impression is wrong, and there have been a few results that have shown theories where one problem, such as unification, is undecidable but another problem, such as deduction, is decidable. These existing dichotomy results were, however, incomplete, and not all cases had been examined, thus leaving the possibility of some connection between the problems for those unexamined cases.

In this paper, we consider the missing dichotomy cases. For each of the remaining cases, we demonstrate a theory that separates the two problems. In addition, once the dichotomy results are completed, it leaves open the question of the existence of non-trivial classes of theories for which all four of the problems are decidable. One example for which this is true is the well-known class of subterm convergent term rewrite systems. In this paper, we develop another example, a class of restrictive permutative theories for which all problems are likewise decidable.

ABSTRACT. Polygraphs play a fundamental role in algebra, geometry, and computer science, by generalizing group presentations to higher-dimensional structures and encoding coherence for those. They have rencently been adapted by Kraus and von Raumer to the setting of homotopy type theory, where they are useful to define and study higher inductive types. Here, we develop the theory of 1-dimensional polygraphs, which correspond to presentations of sets in homotopy type theory. This requires us introducing a dedicated notion of Tietze transformation, generalizing a well-known notion in group theory: the equivalence generated by those transformations characterizes situations when two 1-polygraphs present the same set. We also show a homotopy transfer theorem, which provides a way to transport a coherence structure from one polygraph to another. This lays the foundations for a general theory of polygraphs in arbitrary dimensions, which should be useful for instance to define and study coherent group presentations, allowing for synthetic (co)homology computations. Most of the results in the article have been formalized with the Agda proof assistant using the cubical HoTT library.

ABSTRACT. In type theory based proof assistants, like Coq or Lean or Agda, one can define functions and prove properties about them, so they form an integrated system for programming and proving. This is due to the combination of dependent types and inductive types which, under the Curry-Howard formulas-as-types embedding, allow one to define inductive types with a recursion principle (to define functions by well-founded recursion) and an induction principle (to do proofs by induction).

In polymorphic type theory (system F, also known as lambda-2), it is possible to define inductive data types, such as natural numbers and lists. It is also possible to define coinductive data types such as streams. They work well in the sense that their (co)recursion principles obey the expected computation rules (the beta-rules). In the Calculus of Constructions (lambda-C), which extends polymorphic type theory with dependent types and higher order types, one can state induction principles for inductive data types and coinduction principles for coinductive data types. Unfortunately, these (co)induction principles are not provable in the type theory, because the necessary uniqueness principles are missing (the eta-rules). Awodey, Frey, and Speight (LiCS 2018) use an extension of the Calculus of Constructions with Sigma-types, equality-types, and functional extensionality to provide System F style inductive types with an induction principle by encoding them as a well-chosen subtype, making them initial algebras.

In the present paper, we extend the results of Awodey, Frey, and Speight, to co-inductive types and to general W-types and M-types. To deal with coinductive types, we first define a quotient type that has the desired induction principle. Then we take the quotient of the (system F) definable co-inductive data type with an appropriate equivalence relation. We show that the type obtained is a final coalgebra and thus satisfies the expected coinduction principle, basically stating that bisimilarity and equality coincide. We show this in detail for the well-known type of infinite streams. To emphasize that the approach is general and that we can use the technique for general (co)inductive types, we show that we can define W-types as initial algebras, with an induction principle, and dually, we can define M-types as final coalgebras with a coinduction principle. Categorically, initiality (finality) of an (co)algebra can be stated in various ways and we show that each of these can be used to define an initial (final) (co)algebra in type theory.

ABSTRACT. Ordered, linear, and other substructural type systems allow us to expose deep properties of programs at the syntactic level of types. In this paper, we develop a family of unary logical relations that allow us to prove consequences of parametricity for a range of substructural type systems. A key idea is to parameterize the relation by an algebra, which we exemplify with a monoid and commutative monoid to interpret ordered and linear type systems, respectively. We prove the fundamental theorem of logical relations and apply it to deduce extensional properties of inhabitants of certain types. Examples include demonstrating that the ordered types for list append and reversal are inhabited by exactly one function, as are types of some tree traversals. Similarly, the linear type of the identity function on lists is inhabited only by permutations of the input. Our most advanced example shows that the ordered type of the list fold function is inhabited only by the fold function.

ABSTRACT. Continuation semantics for simple programming languages can be axiomatized as dialogue categories: symmetric monoidal categories equipped with a negation operation. These structures provide a denotational account of CPS transformations, unifying them with game semantics, and covering both call-by-name and call-by-value.

In this paper we extend dialogue categories with 2-categorical structure and primitives for concurrent programming. We build on recent methods for the semantics of concurrent effectful programs, based on 2-categorical concurrent monads. Dialogue categories have special structure not available in generic semantic models, which we exploit to define new concurrent primitives that refine the general framework. Our axiomatization does induce a concurrent continuation 2-monad, but the new primitives are expressive beyond call-by-value monadic programming.

The definitions in this paper are illustrated by concrete constructions in concurrent or asynchronous game semantics, and our results give a formal categorical basis for the concurrent strategies in these models. Our approach also suggests a candidate target language for linear CPS transformations of concurrent programming languages.

ABSTRACT. We introduce higher-dimensional automata for infinite interval ipomsets (omega-HDAs). We define key concepts from different points of view, inspired from their finite counterparts. Then we explore languages recognized by omega-HDAs under Büchi and Muller semantics. We show that Muller acceptance is more expressive than Büchi acceptance and, in contrast to the finite case, both semantics do not yield languages closed under subsumption. Then, we adapt the original rational operations to deal with omega-HDAs and show that while languages of omega-HDAs are omega-rational, not all omega-rational languages can be expressed by omega-HDAs.