Related papers: Extending Equational Monadic Reasoning with Monad …

Proof assistants are software-based tools that are used in the mechanization of proof construction and validation in mathematics and computer science, and also in certified program development. Different tools are being increasingly used in…

We introduce a category-theoreticabstraction of a syntax with auxiliary functions, called an admissiblemonad morphism. Relying on an abstract form of structural recursion,we then design generic tools to construct admissible monad…

We propose a new library to model and verify hardware circuits in the Coq proof assistant. This library allows one to easily build circuits by following the usual pen-and-paper diagrams. We define a deep-embedding: we use a (dependently…

We give a new presentation of interactive realizability with a more explicit syntax. Interactive realizability is a realizability semantics that extends the Curry-Howard correspondence to (sub-)classical logic, more precisely to first-order…

We extend intersection types to a computational $\lambda$-calculus with algebraic operations \`a la Plotkin and Power. We achieve this by considering monadic intersections, whereby computational effects appear not only in the operational…

Contemporary transformer architectures apply identical processing depth to all inputs, creating inefficiencies and limiting reasoning quality. Simple factual queries are subjected to the same multilayered computation as complex logical…

Most existing implementations of multiple precision arithmetic demand that the user sets the precision {\em a priori}. Some libraries are said adaptable in the sense that they dynamically change the precision of each intermediate operation…

This work is a part of an ongoing effort to prove the correctness of invertibility conditions for the theory of fixed-width bit-vectors, which are used to solve quantified bit-vector formulas in the Satisfiability Modulo Theories (SMT)…

Commonsense reasoning has long been considered as one of the holy grails of artificial intelligence. Most of the recent progress in the field has been achieved by novel machine learning algorithms for natural language processing. However,…

This article contains a proposal to add coinduction to the computational apparatus of natural language understanding. This, we argue, will provide a basis for more realistic, computationally sound, and scalable models of natural language…

We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including univalence, higher inductive types, and significant amounts of…

Logical relations and their generalizations are a fundamental tool in proving properties of lambda-calculi, e.g., yielding sound principles for observational equivalence. We propose a natural notion of logical relations able to deal with…

In this paper, we introduce a system called GamePad that can be used to explore the application of machine learning methods to theorem proving in the Coq proof assistant. Interactive theorem provers such as Coq enable users to construct…

This paper is a contribution to the search for efficient and high-level mathematical tools to specify and reason about (abstract) programming languages or calculi. Generalising the reduction monads of Ahrens et al., we introduce transition…

Recent advancements in deep learning have led to the development of powerful language models (LMs) that excel in various tasks. Despite these achievements, there is still room for improvement, particularly in enhancing reasoning abilities…

Analogical reasoning is a hallmark of human intelligence, enabling us to solve new problems by transferring knowledge from one situation to another. Yet, developing artificial intelligence systems capable of robust human-like analogical…

Masked diffusion models (MDMs) for text offer a compelling alternative to traditional autoregressive language models. Parallel generation makes them efficient, but their computational capabilities and the limitations inherent in their…

We prove normalization for MTT, a general multimodal dependent type theory capable of expressing modal type theories for guarded recursion, internalized parametricity, and various other prototypical modal situations. We prove that deciding…

Grokking has been actively explored to reveal the mystery of delayed generalization and identifying interpretable representations and algorithms inside the grokked models is a suggestive hint to understanding its mechanism. Grokking on…

A class of models is presented, in the form of continuation monads polymorphic for first-order individuals, that is sound and complete for minimal intuitionistic predicate logic. The proofs of soundness and completeness are constructive and…