We demonstrate that the checkable/synthesisable split in bidirectional typechecking coincides with existing dualities in polarised System L, also known as polarised $𝜇\widetilde{𝜇}$-calculus. Specifically, positive terms and negative coterms are checkable, and negative terms and positive coterms are synthesisable. This combines a standard formulation of bidirectional typechecking with Zeilberger’s ‘cocontextual’ variant. We extend this to ordinary ‘cartesian’ System L using Mc Bride’s co-de Bruijn formulation of scopes, and show that both can be combined in a linear-nonlinear style, where linear types are positive and cartesian types are negative. This yields a remarkable 3-way coincidence between the shifts of polarised System L, LNL calculi, and bidirectional calculi.

We adapt Fiore, Plotkin, and Turi’s treatment of abstract syntax with binding, substitution, and holes to account for languages with second-class sorts. These situations include programming calculi such as the Call-by-Value lambda-calculus (CBV) and Levy’s Call-by-Push-Value (CBPV). Prohibiting second-class sorts from appearing in variable contexts changes the characterisation of the abstract syntax from monoids in monoidal categories to actions in actegories. We reproduce much of the development through bicategorical arguments. We apply the resulting theory by proving substitution lemmata for varieties of CBV.

Many programs process lists by recursing in a wide variety of sequential and/or divide-and-conquer patterns. Reasoning about the correctness and completeness of these programs requires reasoning about the lengths of the lists, techniques for which are typically undecidable or at least NP-complete. In this paper we show how introducing a relatively simple (sub-)language for expressions describing list lengths, whilst not completely general, covers a great number of these patterns. It includes not only doubling but also exponentiation (iterated doubling), and moreover admits a simple length-checking algorithm that is complete over a predictable problem domain. We prove termination of the algorithm via category-theoretic pullbacks, formalized in Agda, as well as providing a more realistic implementation in Rocq, and a toy language Fulbourn with interpreter in Haskell.

Verification of neural networks is currently a hot topic in automated theorem proving. Progress has been rapid and there are now a wide range of tools available that can verify properties of networks with hundreds of thousands of nodes. In theory this opens the door to the verification of larger control systems that make use of neural network components. However, although work has managed to incorporate the results of these verifiers to prove larger properties of individual systems, there is currently no general methodology for bridging the gap between verifiers and interactive theorem provers (ITPs). In this paper we present Vehicle, our solution to this problem. Vehicle is equipped with an expressive domain specific language for stating neural network specifications which can be compiled to both verifiers and ITPs. It overcomes previous issues with maintainability and scalability in similar ITP formalisations by using a standard ONNX file as the single canonical representation of the network. We demonstrate its utility by using it to connect the neural network verifier Marabou to Agda and then formally verifying that a car steered by a neural network never leaves the road, even in the face of an unpredictable cross wind and imperfect sensors. The network has over 20,000 nodes, and therefore this proof represents an improvement of 3 orders of magnitude over prior proofs about neural network enhanced systems in ITPs.