Related papers: Frex: dependently-typed algebraic simplification
Functional programmers have an established tradition of using traversals as a design pattern to work with recursive data structures. The technique is so prolific that a whole host of libraries have been designed to help in the task of…
Differentiable logics are a family of quantitative logics originated in the machine learning literature. Because of their origin, differentiable logics often come equipped with analytic properties that guarantee that they are…
We find a necessary and sufficient conditions for the simplicity and uniqueness of trace for reduced free products of finite families of finite dimensional $C^*$-algebras with specified traces on them.
The work is devoted to the variety of $2$-dimensional algebras over an algebraically closed field. Firstly, we classify such algebras modulo isomorphism. Then we describe the degenerations and the closures of principal algebra series in the…
Following the types-as-sets paradigm, we present a mechanized embedding of dependent function types with a hierarchy of universes into schematic first-order logic with equality, with axiom schemas of Tarski-Grothendieck set theory. We carry…
This dissertation focuses on the design and the implementation of domain-specific compilers for linear algebra matrix equations. The development of efficient libraries for such equations, which lie at the heart of most software for…
Algebraic specifications of data types provide a natural basis for testing data types implementations. In this framework, the conformance relation is based on the satisfaction of axioms. This makes it possible to formally state the…
A Reduction -- an accumulation over a set of values, using an associative and commutative operator -- is a common computation in many numerical computations, including scientific computations, machine learning, computer vision, and…
We construct a complex entire function with arbitrary number of variables which has the following property: The infinite set consisting of all the values of all its partial derivatives of any orders at all algebraic points, including zero…
Database applications are typically written using a mixture of imperative languages and declarative frameworks for data processing. Application logic gets distributed across the declarative and imperative parts of a program. Often, there is…
One of the aims of Implicit Computational Complexity is the design of programming languages with bounded computational complexity; indeed, guaranteeing and certifying a limited resources usage is of central importance for various aspects of…
Type refinements combine the compositionality of typechecking with the expressivity of program logics, offering a synergistic approach to program verification. In this paper we apply dependent type refinements to SAX, a futures-based…
System F, the polymorphic lambda calculus, features the principle of impredicativity: polymorphic types may be (explicitly) instantiated at other types, enabling many powerful idioms such as Church encoding and data abstraction.…
We present a constructive formalization of Abstract Rewriting Systems (ARS) in the Agda proof assistant, focusing on standard results in term rewriting. We define a taxonomy of concepts related to termination and confluence and investigate…
We describe arithmetic computations in terms of operations on some well known free algebras (S1S, S2S and ordered rooted binary trees) while emphasizing the common structure present in all them when seen as isomorphic with the set of…
The universal-algebraic approach has proved a powerful tool in the study of the complexity of CSPs. This approach has previously been applied to the study of CSPs with finite or (infinite) omega-categorical templates, and relies on two…
While methods of code abstraction and reuse are widespread and well researched, methods of proof abstraction and reuse are still emerging. We consider the use of dependent types for this purpose, introducing a completely mechanical approach…
The Abella interactive theorem prover has proven to be an effective vehicle for reasoning about relational specifications. However, the system has a limitation that arises from the fact that it is based on a simply typed logic:…
We present ZFLean, a Lean 4 library for doing core mathematics inside a model of ZFC with the ergonomics expected of typed Mathlib developments. Building on Mathlib's ZFC model, we contribute a relational calculus for sets with rewriting…
We construct an explicit filtration of the ring of algebraic power series by finite dimensional constructible sets, measuring the complexity of these series. As an application, we give a bound on the dimension of the set of algebraic power…