Related papers: Formalising the Bruhat-Tits Tree
We present three projects concerned with applications of proof assistants in the area of programming language theory and mathematics. The first project is about a certified compilation technique for a domain-specific programming language…
We formalize in Lean the following foundational result in commutative algebra: Let $R \to S$ be a faithfully flat map of (not necessarily noetherian) commutative rings, and let $P$ be an arbitrary $R$-module. Then $P$ is projective over $R$…
The boolean elements of a Coxeter group have been characterized and shown to possess many interesting properties and applications. Here we introduce "prism permutations," a generalization of those elements, characterizing the prism…
In "Hopf algebra of the planar binary trees", Adv. Math. 139 (1998), no. 2, 293--309, we constructed by induction a graded associative product on the vector space generated by the planar binary trees (resp. the permutations). In the present…
We propose a new formalism for quantum field theory which is neither based on functional integrals, nor on Feynman graphs, but on marked trees. This formalism is constructive, i.e. it computes correlation functions through convergent rather…
This extended abstract is about an effort to build a formal description of a triangulation algorithm starting with a naive description of the algorithm where triangles, edges, and triangulations are simply given as sets and the most complex…
Behavior Trees (BT) are becoming quite popular as an Acting component of autonomous robotic systems. We propose to define a formal semantics to BT by translating them to a formal language which enables us to perform verification of programs…
Termination is an important property of programs; notably required for programs formulated in proof assistants. It is a very active subject of research in the Turing-complete formalism of term rewriting systems, where many methods and tools…
The establishment of trust relationships to a computing platform relies on validation processes. Validation allows an external entity to build trust in the expected behaviour of the platform based on provided evidence of the platform's…
This paper explores formalizing Geometric (or Clifford) algebras into the Lean 3 theorem prover, building upon the substantial body of work that is the Lean mathematics library, mathlib. As we use Lean source code to demonstrate many of our…
We describe a formalization of forcing using Boolean-valued models in the Lean 3 theorem prover, including the fundamental theorem of forcing and a deep embedding of first-order logic with a Boolean-valued soundness theorem. As an…
The use of formal methods provides confidence in the correctness of developments. Yet one may argue about the actual level of confidence obtained when the method itself -- or its implementation -- is not formally checked. We address this…
We present a formal framework for proving the correctness of set implementations backed by binary-search-tree (BST) and linked lists, which are often difficult to prove correct using automation. This is because many concurrent set…
An informal discussion of how the construction problem in algebraic geometry motivates the search for formal proof methods. Also includes a brief discussion of my own progress up to now, which concerns the formalization of category theory…
In this article, we present an effective encoding of dendrograms by embedding them into the Bruhat-Tits trees associated to $p$-adic number fields. As an application, we show how strings over a finite alphabet can be encoded in cyclotomic…
In this paper we use formal group rings to construct an algebraic model of the $T$-equivariant oriented cohomology of smooth toric varieties. Then we compare our model with known results of equivariant cohomology of toric varieties to…
Knowledge representation and reasoning in law are essential to facilitate the automation of legal analysis and decision-making tasks. In this paper, we propose a new approach based on legal science, specifically legal taxonomy, for…
The adele ring of a number field is a central object in modern number theory. Its status as a locally compact topological ring is one of the key reasons why. We describe a formal proof that the adele ring of a number field is locally…
[Context & motivation] Eliciting requirements that are detailed and logical enough to be amenable to formal verification is a difficult task. Multiple tools exist for requirements elicitation and some of these also support formalisation of…
Interactive proof assistants are computer programs carefully constructed to check a human-designed proof of a mathematical claim with high confidence in the implementation. However, this only validates truth of a formal claim, which may…