A type of higher-order two-dimensional sketch is defined which has models in suitable 2-categories. It has as special cases the ordinary sketches of Ehresmann and certain previously defined generalizations of one-dimensional sketches. These sketches allow the specification of constructions in 2-categories such as weighted limits, as well as higher-order constructions such as exponential objects and subobject classifiers, that cannot be sketched by limits and colimits. These sketches are designed to be the basis of a category-based methodology for the description of functional programming languages, complete with rewrite rules giving the operational semantics, that is independent of the usual specification methods based on formal languages and symbolic logic. A definition of ‘path grammar’, generalizing the usual notion of grammar, is given as a step towards this goal.

By the Final Coalgebra Theorem of Aczel and Mendler, every endofunctor of the category of sets has a final coalgebra, which, however, may be a proper class. We generalise this to all ‘well-behaved’ categories ${\frak K}$. The role of the category of classes is played by a free cocompletion ${\frak K}^\infty$ of ${\frak K}$ under transfinite colimits, that is, colimits of ordinal-indexed chains. Every endofunctor $F$ of ${\frak K}$ has a canonical extension to an endofunctor $F^\infty$ of ${\frak K}^\infty$, which is proved to have a final coalgebra (and an initial algebra). Based on this, we prove a general solution theorem: for every endofunctor of a locally presentable category ${\frak K}$ all guarded equation-morphisms have unique solutions. The last result does not need the extension ${\frak K}^\infty$: the solutions are always found within the category ${\frak K}$.

We show how to apply forward and reverse mode Combinatory Homomorphic Automatic Differentiation (CHAD) (Vákár (2021). ESOP, 607–634; Vákár and Smeding (2022). ACM Transactions on Programming Languages and Systems 44 (3) 20:1–20:49.) to total functional programming languages with expressive type systems featuring the combination of

• • tuple types;

• • sum types;

• • inductive types;

• • coinductive types;

• • function types.

We achieve this by analyzing the categorical semantics of such types in $\Sigma$-types (Grothendieck constructions) of suitable categories. Using a novel categorical logical relations technique for such expressive type systems, we give a correctness proof of CHAD in this setting by showing that it computes the usual mathematical derivative of the function that the original program implements. The result is a principled, purely functional and provably correct method for performing forward- and reverse-mode automatic differentiation (AD) on total functional programming languages with expressive type systems.

This work extends a rule-based specification of nominal C-unification formalised in Coq to include ‘protected variables’ that cannot be instantiated during the unification process. By introducing protected variables, we are able to reuse the C-unification simplification rules to solve nominal C-matching (as well as equality check) problems. From the algorithmic point of view, this extension is sufficient to obtain a generalised C-unification procedure; however, it cannot be formally checked by simple reuse of the original formalisation. This paper describes the additional effort necessary in order to adapt the specification of the inference rules and reuse previous formalisations. We also generalise a functional recursive nominal C-unification algorithm specified in PVS with protected variables, effectively adapting this algorithm to the tasks of nominal C-matching and nominal equality check. The PVS formalisation is applied to test the correctness of a Python manual implementation of the algorithm.

This paper deals with the specification problem in classical realizability (such as introduced by Krivine (2009 Panoramas et synthéses27)), which is to characterize the universal realizers of a given formula by their computational behaviour. After recalling the framework of classical realizability, we present the problem in the general case and illustrate it with some examples. In the rest of the paper, we focus on Peirce's law, and present two game-theoretic characterizations of its universal realizers. First, we consider the particular case where the language of realizers contains no extra instruction such as ‘quote’ (Krivine 2003 Theoretical Computer Science308 259–276). We present a first game $\mathds{G}$0 and show that the universal realizers of Peirce's law can be characterized as the uniform winning strategies for $\mathds{G}$0, using the technique of interaction constants. Then we show that in the presence of extra instructions such as ‘quote’, winning strategies for the game $\mathds{G}$0 are still adequate but no more complete. For that, we exhibit an example of a wild realizer of Peirce's law, that introduces a purely game-theoretic form of backtrack that is not captured by $\mathds{G}$0. We finally propose a more sophisticated game $\mathds{G}$1, and show that winning strategies for the game $\mathds{G}$1 are both adequate and complete in the general case, without any further assumption about the instruction set used by the language of classical realizers.

Type isomorphisms are pairs of functions $f:A\rightarrow B$ and $g:B\rightarrow A$ that are mutually inverse with respect to convertibility. They can be used in the context of type checking to perform type checking modulo type isomorphisms, by adopting the rule $$\frac{a:A}{a:B}$$ whenever $f:A\rightarrow B$ and $g:B\rightarrow A$ have been declared as type isomorphisms. Type isomorphisms may be viewed as a special instance of coercions that provide embeddings of one type into another. Indeed, type systems for coercive subtyping feature a rule $$\frac{a:A}{a:B}$$ whenever there exists a coercion $f:A\rightarrow B$. By declaring $f$ and $g$ as coercions for every type isomorphism $f:A\rightarrow B$ and $g:B\rightarrow A$, one can simulate type-checking modulo type isomorphisms. However, the proposed encoding relies on the possibility of declaring coercions $f:A\rightarrow B$ and $g:B\rightarrow A$ simultaneously. Such coercions, which we call back-and-forth coercions, are only allowed provided $f$ and $g$ are mutually inverse. In principle, type isomorphisms, viewed as back-and-forth coercions, could be used in the context of proof assistants based on dependent type theory in order to relate equivalent representations of mathematical notions, for example, the polar and cartesian representations of complex numbers. However, the coercions that map one representation into another are not mutually inverse because of the intensional nature of dependent type theories. Consequently, the standard concept of type isomorphisms has limited applicability in the context of proof assistants.

In order to circumvent this problem, we develop a computational interpretation of implicit coercions that allows for the definition of back-and-forth coercions without requiring them to be mutually inverse. We illustrate the usefulness of our approach in a number of formal developments that require us to navigate between different representations of mathematical objects or structures. We also discuss important meta-theoretical properties of our interpretation.

We consider matching, rewriting, critical pairs and the Knuth–Bendix confluence test on rewrite rules in a nominal setting extended by atom-variables. We utilize atom-variables instead of atoms to formulate and rewrite rules on constrained expressions, which is an improvement of expressiveness over previous approaches. Nominal unification and nominal matching are correspondingly extended. Rewriting is performed using nominal matching, and computing critical pairs is done using nominal unification. We determine the complexity of several problems in a quantified freshness logic. In particular we show that nominal matching is $$\prod _2^p$$ -complete. We prove that the adapted Knuth–Bendix confluence test is applicable to a nominal rewrite system with atom-variables, and thus that there is a decidable test whether confluence of the ground instance of the abstract rewrite system holds. We apply the nominal Knuth–Bendix confluence criterion to the theory of monads and compute a convergent nominal rewrite system modulo alpha-equivalence.

We prove that the semantics of intuitionistic linear logic in vector spaces which uses cofree coalgebras is also a model of differential linear logic, and that the Cartesian closed category of cofree coalgebras is a model of the simply typed differential λ-calculus.

This paper introduces and studies a categorical analogue of the familiar monoid semiring construction. By introducing an axiomatisation of summation that unifies notions of summation from algebraic program semantics with various notions of summation from the theory of analysis, we demonstrate that the monoid semiring construction generalises to cases where both the monoid and the semiring are categories. This construction has many interesting and natural categorical properties, and natural computational interpretations.

We study logic in the light of the Kantian distinction between analytic (untyped, meaningless, locative) answers and synthetic (typed, meaningful, spiritual) questions. Which is specially relevant to proof-theory: in a proof-net, the upper part is locative, whereas the lower part is spiritual: a posteriori (explicit) as far as correctness is concerned, a priori (implicit) for questions dealing with consequence, typically cut-elimination. The divides locative/spiritual and explicit/implicit give rise to four blocks which are enough to explain the whole logical activity.

Natural restrictions on the syntax of the second-order (i.e., polymorphic) lambda calculus are of interest for programming language theory. One of the authors showed in Leivant (1991) that when type abstraction in that calculus is stratified into levels, the definable numeric functions are precisely the super-elementary functions (level [Escr ]4 in the Grzegorczyk Hierarchy). We define here a second-order lambda calculus in which type abstraction is stratified to levels up to ωω, an ordinal that permits highly uniform (and finite) type inference rules. Referring to this system, we show that the numeric functions definable in the calculus using ranks < ω[lscr ] are precisely Grzegorczyk's class [Escr ][lscr ]+3 ([lscr ] [ges ] 1). This generalizes Leivant (1991), where this is proved for [lscr ] = 1. Thus, the numeric functions definable in our calculus are precisely the primitive recursive functions.

In constructive theories, an apartness relation is often taken as basic and its negation used as equality. An apartness relation should be continuous in its arguments, as in the case of computable reals. A similar approach can be taken to order relations. We shall here study the partial order on open intervals of computable reals. Since order on reals is undecidable, there is no simple uniformly applicable lattice meet operation that would always produce non-negative intervals as values. We show how to solve this problem by a suitable definition of apartness for intervals. We also prove the strong extensionality of the lattice operations, where by strong extensionality of an operation f on elements a, b we mean that apartness of values implies apartness in some of the arguments: f(a, b)≠f(c, d) ⊃a≠c∨b≠d.

Most approaches to computable reals start from a concrete definition. We shall instead represent them by an abstract axiomatically introduced order structure.

Software watermarking is a software protection technique used to defend the intellectual property of proprietary code. In particular, software watermarking aims at preventing software piracy by embedding a signature, i.e. an identifier reliably representing the owner, in the code. When an illegal copy is made, the owner can claim his/her identity by extracting the signature. It is important to hide the signature in the program in order to make it difficult for the attacker to detect, tamper or remove it. In this work, we present a formal framework for software watermarking, based on program semantics and abstract interpretation, where attackers are modelled as abstract interpreters. In this setting, we can prove that the ability to identify signatures can be modelled as a completeness property of the attackers in the abstract interpretation framework. Indeed, hiding a signature in the code corresponds to embed it as a semantic property that can be retrieved only by attackers that are complete for it. Any abstract interpreter that is not complete for the property specifying the signature cannot detect, tamper or remove it. We formalize in the proposed framework the major quality features of a software watermarking technique: secrecy, resilience, transparence and accuracy. This provides a unifying framework for interpreting both watermarking schemes and attacks, and it allows us to formally compare the quality of different watermarking techniques. Indeed, a large number of watermarking techniques exist in the literature and they are typically evaluated with respect to their secrecy, resilience, transparence and accuracy to attacks. Formally identifying the attacks for which a watermarking scheme is secret, resilient, transparent or accurate can be a complex and error-prone task, since attacks and watermarking schemes are typically defined in different settings and using different languages (e.g. program transformation vs. program analysis), complicating the task of comparing one against the others.

We investigate the issues of existence and efficiency of lookahead equilibria in congestion games. Lookahead equilibria, whose study has been initiated by Mirrokni et al. (2012), correspond to the natural extension of pure Nash equilibria in which the players, when making use of global information in order to predict subsequent reactions of the other ones, have computationally limited capabilities.

Given a monoidal category $\mathcal C$ with an object J, we construct a monoidal category $\mathcal C[{J^ \vee }]$ by freely adjoining a right dual ${J^ \vee }$ to J. We show that the canonical strong monoidal functor $\Omega :\mathcal C \to \mathcal C[{J^ \vee }]$ provides the unit for a biadjunction with the forgetful 2-functor from the 2-category of monoidal categories with a distinguished dual pair to the 2-category of monoidal categories with a distinguished object. We show that $\Omega :\mathcal C \to \mathcal C[{J^ \vee }]$ is fully faithful and provide coend formulas for homs of the form $\mathcal C[{J^ \vee }](U,\,\Omega A)$ and $\mathcal C[{J^ \vee }](\Omega A,U)$ for $A \in \mathcal C$ and $U \in \mathcal C[{J^ \vee }]$. If ${\rm{N}}$ denotes the free strict monoidal category on a single generating object 1, then ${\rm{N[}}{{\rm{1}}^ \vee }{\rm{]}}$ is the free monoidal category Dpr containing a dual pair – ˧ + of objects. As we have the monoidal pseudopushout $\mathcal C[{J^ \vee }] \simeq {\rm{Dpr}}{{\rm{ + }}_{\rm{N}}}\mathcal C$, it is of interest to have an explicit model of Dpr: we provide both geometric and combinatorial models. We show that the (algebraist’s) simplicial category Δ is a monoidal full subcategory of Dpr and explain the relationship with the free 2-category Adj containing an adjunction. We describe a generalization of Dpr which includes, for example, a combinatorial model Dseq for the free monoidal category containing a duality sequence X0 ˧ X1 ˧ X2 ˧ … of objects. Actually, Dpr is a monoidal full subcategory of Dseq.

We define a notion of homotopy in the effective topos.

The programs, we consider are written in a restricted form of the language introduced by Dijkstra (1968). A program is said to be conservative when each of its loops restores all the resources it consumes. We define the geometric model of such a program and prove that the collection of directed paths on it is a reasonable over-approximation of its set of execution traces. In particular, two directed paths that are close enough with respect to the uniform distance result in the same action on the memory states of the system. The same holds for weakly dihomotopic directed paths. As a by-product, we obtain a notion of independence, which is favourably compared to more common ones. The geometric models actually belong to a handy class of local pospaces whose elements are called isothetic regions. The local pospaces we use differ from the original ones, we carefully explain why the alternative notion should be preferred. The title intentionally echoes the article by Carson and Reynolds (1987).

Type theory allows us to extract from a constructive proof that a specification is satisfiable a program that satisfies the specification. Algorithms for optimization of such programs are currently the object of research.

In this paper we consider one such algorithm, which was described in Beeson (1985) and which we will call ‘Harrop’. This algorithm greatly simplifies programs extracted from proofs in the Pure Construction Calculus. We use a Partial Equivalence Relation model for higher order lambda calculus, to check that t and Harrop(t) return the same outputs from the same inputs, i.e. that they are extensionally equal.

As a corollary, we show that it is correct (and, of course, useful) to replace a program t with Harrop(t). Such a correctness result has already been proved by Möhring (Möhring 1989a, 1989b) using realizability semantics, but we obtain it as a corollary of a new result, the extensional equality between t and Harrop(t). Also the semantic method we use is interesting in its own right.

This work concerns the representation of a class of continuous functions into Logic, so that one may automatically reason about properties of these functions using logical tools. Rational McNaughton functions may be implicitly represented by logical formulas in Łukasiewicz Infinitely-valued Logic by constraining the set of allowed valuations; such a restriction contemplates only those valuations that satisfy specific formulas. This work investigates two approaches to such depiction, called representation modulo satisfiability. Furthermore, a polynomial-time algorithm that builds this representation is presented, producing a pair of formulas consisting of the representative formula and the constraining one, given as input a rational McNaughton function in a suitable encoding. An implementation of the algorithm is discussed.