Related papers: Concrete Semantics with Coq and CoqHammer
Classes on compiler technology are commonly found in Computer Science curricula, covering aspects of parsing, semantic analysis, intermediate transformations and target code generation. This paper reports on introducing certified…
Quantum computing (QC) represents the future of computing systems, but the tools for reasoning about the quantum model of computation, in which the laws obeyed are those on the quantum mechanical scale, are still a mix of linear algebra and…
Should the final right bracket in a record declaration be on a separate line? Should arguments to the rewrite tactic be separated by a single space? Coq code tends to be written in distinct manners by different people and teams. The…
In order to help students learn how to write mathematical proofs, we adapt the Coq proof assistant into an educational tool we call Waterproof. Like with other interactive theorem provers, students write out their proofs inside the software…
The importance of category theory in recent developments in both mathematics and in computer science cannot be overstated. However, its abstract nature makes it difficult to understand at first. Graphical languages have been developed to…
While the use of formal verification techniques is well established in the development of mission-critical software, it is still rare in the production of most other kinds of software. We share our experience that a formal verification tool…
We argue that the implementation and verification of compilers for functional programming languages are greatly simplified by employing a higher-order representation of syntax known as Higher-Order Abstract Syntax or HOAS. The underlying…
Verification proofs encode complete program behavior, yet we discard them after checking correctness. We present compiling by proving, a paradigm that transforms these proofs into optimized execution rules. By constructing All-Path…
This report presents a formalization of May's theorem in the proof assistant Coq. It describes how the theorem statement is first translated into Coq definitions, and how it is subsequently proved. Various aspects of the proof and related…
The research in AI-based formal mathematical reasoning has shown an unstoppable growth trend. These studies have excelled in mathematical competitions like IMO and have made significant progress. This paper focuses on formal verification,…
We present a novel definition of an algorithm and its corresponding algorithm language called CoLweb. The merit of CoLweb [1] is that it makes algorithm design so versatile. That is, it forces us to a high-level, proof-carrying,…
Adding rewriting to a proof assistant based on the Curry-Howard isomorphism, such as Coq, may greatly improve usability of the tool. Unfortunately adding an arbitrary set of rewrite rules may render the underlying formal system undecidable…
One important approach to software verification is interactive theorem proving. However, writing formal proofs often requires substantial human effort, making proof automation highly important. Traditionally, proof automation has relied on…
We report on our formalization of matrix-interpretation in Isabelle/HOL. Matrices are required to certify termination proofs and we wish to utilize them for complexity proofs, too. For the latter aim, only basic methods have already been…
Isabelle is a generic theorem prover with a fragment of higher-order logic as a metalogic for defining object logics. Isabelle also provides proof terms. We formalize this metalogic and the language of proof terms in Isabelle/HOL, define an…
An invaluable feature of computer algebra systems is their ability to plot the graph of functions. Unfortunately, when one is trying to design a library of mathematical functions, this feature often falls short, producing incorrect and…
We have previously published the Isabelle/HOL formalization of a general theory of syntax with bindings. In this companion paper, we instantiate the general theory to the syntax of lambda-calculus and formalize the development leading to…
We address the challenges of scaling verification efforts to match the increasing complexity and size of systems. We propose a research agenda aimed at building a performant proof engine by studying the asymptotic performance of proof…
In order to increase user confidence, many automated theorem provers provide certificates that can be independently verified. In this paper, we report on our progress in developing a standalone tool for checking the correctness of…
To obtain the highest confidence on the correction of numerical simulation programs implementing the finite element method, one has to formalize the mathematical notions and results that allow to establish the soundness of the method.…