Related papers: Kleene Algebra with Tests and Coq Tools for While …
We describe several views of the semantics of a simple programming language as formal documents in the calculus of inductive constructions that can be verified by the Coq proof system. Covered aspects are natural semantics, denotational…
We show how concurrent quantales and concurrent Kleene algebras arise as convolution algebras $Q^X$ of functions from structures $X$ with two ternary relations that satisfy relational interchange laws into concurrent quantales or Kleene…
We extend the formalisation of confluence results in Kleene algebras to a formalisation of coherent confluence proofs. For this, we introduce the structure of higher globular Kleene algebra, a higher-dimensional generalisation of modal and…
We give a number of formal proofs of theorems from the field of computable analysis. Many of our results specify executable algorithms that work on infinite inputs by means of operating on finite approximations and are proven correct in the…
Program logics are a powerful formal method in the context of program verification. Can we develop a counterpart of program logics in the context of language verification? This paper proposes language logics, which allow for statements of…
Convex polyhedral abstractions of logic programs have been found very useful in deriving numeric relationships between program arguments in order to prove program properties and in other areas such as termination and complexity analysis. We…
In relational verification, judicious alignment of computational steps facilitates proof of relations between programs using simple relational assertions. Relational Hoare logics (RHL) provide compositional rules that embody various…
For performance and verification in machine learning, new methods have recently been proposed that optimise learning systems to satisfy formally expressed logical properties. Among these methods, differentiable logics (DLs) are used to…
We give a method to transform into programs, classical proofs using a well ordering of the reals. The technics uses a generalization of Cohen's forcing and the theory of classical realizability introduced by the author.
It is shown that antidomain semirings are more expressive than test semirings and that Kleene algebras with domain are more expressive than Kleene algebras with tests. It is also shown that Kleene algebras with domain are expressive for…
Distributive laws are important for algebraic reasoning in arithmetic and logic. They are equally important for algebraic reasoning about concurrent programs. In existing theories such as Concurrent Kleene Algebra, only partial correctness…
The syntax of an imperative language does not mention explicitly the state, while its denotational semantics has to mention it. In this paper we present a framework for the verification in Coq of properties of programs manipulating the…
We describe our experience implementing a broad category-theory library in Coq. Category theory and computational performance are not usually mentioned in the same breath, but we have needed substantial engineering effort to teach Coq to…
The ever-growing complexity of mathematical proofs makes their manual verification by mathematicians very cognitively demanding. Autoformalization seeks to address this by translating proofs written in natural language into a formal…
There are several ways to define program equivalence for functional programs with algebraic effects. We consider two complementing ways to specify behavioural equivalence. One way is to specify a set of axiomatic equations, and allow proof…
Exception handling is provided by most modern programming languages. It allows to deal with anomalous or exceptional events which require special processing. In computer algebra, exception handling is an efficient way to implement the…
A Kleene semiring is an algebraic structure satisfying the axioms of Kleene algebra, minus the annihilation axioms (x.0 = 0 = 0.x). We show that Kleene semirings (like Kleene algebras) admit the efficient elimination of various kinds of…
We propose a simple, yet expressive proof representation from which proofs for different proof assistants can easily be generated. The representation uses only a few inference rules and is based on a frag- ment of first-order logic called…
We describe how we connected three programs that compute Groebner bases to Coq, to do automated proofs on algebraic, geometrical and arithmetical expressions. The result is a set of Coq tactics and a certificate mechanism (downloadable at…
In the realm of formal theorem proving, the Coq proof assistant stands out for its rigorous approach to verifying mathematical assertions and software correctness. Despite the advances in artificial intelligence and machine learning, the…