In homotopy type theory, few constructions have proved as troublesome as the smash product. While its definition is just as direct as in classical mathematics, one quickly realises that in order to define and reason about functions over iterations of it, one has to verify an exponentially growing number of coherences. This has led to crucial results concerning smash products remaining open. One particularly important such result is the fact that the smash product forms a (1-coherent) symmetric monoidal product on the universe of pointed types. This fact was used, without a complete proof, by, for example, Brunerie ((2016) PhD thesis, Université Nice Sophia Antipolis) to construct the cup product on integral cohomology and is, more generally, a fundamental result in traditional algebraic topology. In this paper, we salvage the situation by introducing a simple informal heuristic for reasoning about functions defined over iterated smash products. We then use the heuristic to verify, for example, the hexagon and pentagon identities, thereby obtaining a proof of symmetric monoidality. We also provide a formal statement of the heuristic in terms of an induction principle concerning the construction of homotopies of functions defined over iterated smash products. The key results presented here have been formalised in the proof assistant Cubical Agda.

We give a simple, direct, and reusable logical relations technique for languages with term and type recursion and partially defined differentiable functions. We demonstrate it by working out the case of automatic differentiation (AD) correctness: namely, we present a correctness proof of a dual numbers style AD code transformation for realistic functional languages in the ML-family. We also show how this code transformation provides us with correct forward- and reverse-mode AD.

The starting point is to interpret a functional programming language as a suitable freely generated categorical structure. In this setting, by the universal property of the syntactic categorical structure, the dual numbers AD code transformation and the basic $\boldsymbol{\omega } \mathbf{Cpo}$-semantics arise as structure preserving functors. The proof follows, then, by a novel logical relations argument.

The key to much of our contribution is a powerful monadic logical relations technique for term recursion and recursive types. It provides us with a semantic correctness proof based on a simple approach for denotational semantics, making use only of the very basic concrete model of $\omega$-cpos.

Perfect paradefinite algebras are De Morgan algebras expanded with an operation that allows for the full behavior of classical negation to be restored. They form a variety that is term-equivalent to the variety of involutive Stone algebras. Their associated multiple-conclusion (Set-Set) and single-conclusion () order-preserving logics are non-algebraizable self-extensional logics of formal inconsistency and undeterminedness determined by a six-valued matrix. We studied these logics extensively in Gomes et al. ((2022). Electronic Proceedings in Theoretical Computer Science 357 56–76.) from both the algebraic and the proof-theoretical perspectives. In the present paper, we continue that study by investigating directions for conservatively expanding these logics with an implication connective (essentially, one that admits the deduction-detachment theorem). We first consider logics given by very simple and manageable non-deterministic semantics whose implication (in isolation) is classical. These, nevertheless, fail to be self-extensional. We then consider the implication realized by the relative pseudo-complement over the six-valued perfect paradefinite algebra. Our strategy is to expand the language of the latter algebra with this connective and study the (self-extensional) Set-Set and order-preserving and $\top$-assertional logics of the variety induced by the resulting algebra. We provide axiomatizations for such new variety and for such logics, drawing parallels with the class of symmetric Heyting algebras and with Moisil’s “symmetric modal logic.” For the order-preserving Set-Set logic, in particular, we obtain a Set-Set axiomatization that is analytic. We close by studying interpolation properties for these logics and concluding that the new variety has the Maehara amalgamation property.

We discuss the complexity of completions of partial combinatory algebras, in particular, of Kleene’s first model. Various completions of this model exist in the literature, but all of them have high complexity. We show that although there are no computable completions, there exist completions of low Turing degree. We use this construction to relate completions of Kleene’s first model to complete extensions of $\mathrm{PA}$. We also discuss the complexity of pcas defined from nonstandard models of $\mathrm{PA}$.

One of the elegant achievements in the history of proof theory is the characterization of the provably total recursive functions of an arithmetical theory by its proof-theoretic ordinal as a way to measure the time complexity of the functions. Unfortunately, the machinery is not sufficiently fine-grained to be applicable on the weak theories, on the one hand and to capture the bounded functions with bounded definitions of strong theories, on the other. In this paper, we develop such a machinery to address the bounded theorems of both strong and weak theories of arithmetic. In the first part, we provide a refined version of ordinal analysis to capture the feasibly definable and bounded functions that are provably total in $\textrm{PA}+\bigcup _{\beta \prec \alpha } \textrm{TI}({\prec_{\beta}})$, the extension of Peano arithmetic by transfinite induction up to the ordinals below $\alpha$. Roughly speaking, we identify the functions as the ones that are computable by a sequence of $\textrm{PV}$-provable polynomial time modifications on an initial polynomial time value, where the computational steps are indexed by the ordinals below $\alpha$, decreasing by the modifications. In the second part, and choosing $l \leq k$, we use similar technique to capture the functions with bounded definitions in the theory $T^k_2$ (resp. $S^k_2$) as the functions computable by exponentially (resp. polynomially) long sequence of $\textrm{PV}_{k-l +1}$-provable reductions between $l$-turn games starting with an explicit $\textrm{PV}_{k-l +1}$-provable winning strategy for the first game.

We take another look at the construction by Hofmann and Streicher of a universe $(U,{\mathcal{E}l})$ for the interpretation of Martin-Löf type theory in a presheaf category $[{{{\mathbb{C}}}^{\textrm{op}}},\textsf{Set}]$. It turns out that $(U,{\mathcal{E}l})$ can be described as the nerve of the classifier $\dot{{\textsf{Set}}}^{\textsf{op}} \rightarrow{{\textsf{Set}}}^{\textsf{op}}$ for discrete fibrations in $\textsf{Cat}$, where the nerve functor is right adjoint to the so-called “Grothendieck construction” taking a presheaf $P :{{{\mathbb{C}}}^{\textrm{op}}}\rightarrow{\textsf{Set}}$ to its category of elements $\int _{\mathbb{C}} P$. We also consider change of base for such universes, as well as universes of structured families, such as fibrations.

The authors’ primary goal in this paper is to enhance the study of $T_0$ topological spaces by using the order of specialization of a $T_0$-space to introduce the lower topology (with a subbasis of closed sets $\mathord{\uparrow } x$) and studying the interaction of the original topology and the lower topology. Using the lower topology, one can define and study new properties of the original space that provide deeper insight into its structure. One focus of study is the property R, which asserts that if the intersection of a family of finitely generated sets $\mathord{\uparrow } F$, $F$ finite, is contained in an open set $U$, then the same is true for finitely many of the family. We first show that property R is equivalent to several other interesting properties, for example, the property that all closed subsets of the original space are compact in the lower topology. We then find conditions under which these spaces are compact, well-filtered, and coherent, a weaker variant of stably compact spaces. We also investigate what have been called strong $d$-spaces, develop some of their basic properties, and make connections with the earlier considerations involving spaces satisfying property R. Two key results we obtain are that if a dcpo $P$ with the Scott topology is a strong $d$-space, then it is well-filtered, and if additionally the Scott topology of the product $P\times P$ is the product of the Scott topologies of the factors, then the Scott space of $P$ is sober. We also exhibit connections of this work with de Groot duality.

Generalized Algebraic Data Types (GADTs) are a syntactic generalization of the usual algebraic data types (ADTs), such as lists, trees, etc. ADTs’ standard initial algebra semantics (IAS) in the category $\mathit{Set}$ of sets justify critical syntactic constructs – such as recursion, pattern matching, and fold – for programming with them. In this paper, we show that semantics for GADTs that specialize to the IAS for ADTs are necessarily unsatisfactory. First, we show that the functorial nature of such semantics for GADTs in $\mathit{Set}$ introduces ghost elements, i.e., elements not writable in syntax. Next, we show how such ghost elements break parametricity. We observe that the situation for GADTs contrasts dramatically with that for ADTs, whose IAS coincides with the parametric model constructed via their Church encodings in System F. Our analysis reveals that the fundamental obstacle to giving a functorial IAS for GADTs is the inherently partial nature of their map functions. We show that this obstacle cannot be overcome by replacing $\mathit{Set}$ with other categories that account for this partiality.

We present a linearity theorem for a proof language of intuitionistic multiplicative additive linear logic, incorporating addition and scalar multiplication. The proofs in this language are linear in the algebraic sense. This work is part of a broader research program aiming to define a logic with a proof language that forms a quantum programming language.

Computability on uncountable sets has no standard formalization, unlike that on countable sets, which is given by Turing machines. Some of the approaches to define computability in these sets rely on order-theoretic structures to translate such notions from Turing machines to uncountable spaces. Since these machines are used as a baseline for computability in these approaches, countability restrictions on the ordered structures are fundamental. Here, we show several relations between the usual countability restrictions in order-theoretic theories of computability and some more common order-theoretic countability constraints, like order density properties and functional characterizations of the order structure in terms of multi-utilities. As a result, we show how computability can be introduced in some order structures via countability order density and multi-utility constraints.

Cyclic proof systems permit derivations that are finite graphs in contrast to conventional derivation trees. The soundness of such proofs is ensured by imposing a soundness condition on derivations. The most common such condition is the global trace condition (GTC), a condition on the infinite paths through the derivation graph. To give a uniform treatment of such cyclic proof systems, Brotherston proposed an abstract notion of trace. We extend Brotherston’s approach into a category theoretical rendition of cyclic derivations, advancing the framework in two ways: first, we introduce activation algebras which allow for a more natural formalisation of trace conditions in extant cyclic proof systems. Second, accounting for the composition of trace information allows us to derive novel results about cyclic proofs, such as introducing a Ramsey-style trace condition. Furthermore, we connect our notion of trace to automata theory and prove that verifying the GTC for abstract cyclic proofs with certain trace conditions is PSPACE-complete.

It is known that without synchronization via a global clock one cannot obtain common knowledge by communication. Moreover, it is folklore that without communicating higher-level information one cannot obtain arbitrary higher-order shared knowledge. Here, we make this result precise in the setting of gossip where agents make one-to-one telephone calls to share secrets: we prove that “everyone knows that everyone knows that everyone knows all secrets” is unsatisfiable in a logic of knowledge for gossiping. We also prove that, given n agents, $2n-3$ calls are optimal to reach “someone knows that everyone knows all secrets” and that $n - 2 + \binom{n}{2}$ calls are optimal to reach “everyone knows that everyone knows all secrets.”

Although reasoning about equations over strings has been extensively studied for several decades, little research has been done for equational reasoning on general clauses over strings. This paper introduces a new superposition calculus with strings and present an equational theorem proving framework for clauses over strings. It provides a saturation procedure for clauses over strings and show that the proposed superposition calculus with contraction rules is refutationally complete. In particular, this paper presents a new decision procedure for solving word problems over strings and provides a new method of solving unification problems over strings w.r.t. a set of conditional equations R over strings if R can be finitely saturated under the proposed inference system with contraction rules.

We show that Kozen and Tiuryn’s substructural logic of partial correctness $\mathsf{S}$ embeds into the equational theory of Kleene algebra with domain, $\mathsf{KAD}$. We provide an implicational formulation of $\mathsf{KAD}$ which sets $\mathsf{S}$ in the context of implicational extensions of Kleene algebra.

Social media is not a neutral channel. How visible information posted online is depends on many factors such as the network structure, the emotional volatility of the content, and the design of the social media platform. In this paper, we use formal methods to study the visibility of agents and information in a social network, as well as how vulnerable the network is to exploitation. We introduce a modal logic to reason about a social network of agents that can follow each other, post, and share information. We show that by imposing some simple rules on the system, a potentially malicious agent can take advantage of the network construction to post an unpopular opinion that may reach many agents. The network is presented both in static and dynamic forms. We prove completeness, expressivity, and model checking problem complexity results for the corresponding logical systems.

Dialogues are turn-taking games which model debates about the satisfaction of logical formulas. A novel variant played over first-order structures gives rise to a notion of first-order satisfaction. We study the induced notion of validity for classical and intuitionistic first-order logic in the constructive setting of the calculus of inductive constructions. We prove that such material dialogue semantics for classical first-order logic admits constructive soundness and completeness proofs, setting it apart from standard model-theoretic semantics of first-order logic. Furthermore, we prove that completeness with regard to intuitionistic material dialogues fails in both constructive and classical settings. As an alternative, we propose material dialogues played over Kripke structures. These Kripke material dialogues exhibit constructive completeness when restricting to the negative fragment. The results concerning classical material dialogues have been mechanized using the Coq interactive theorem prover.