Related papers: Constructive Analysis in the Agda Proof Assistant
Real-life conjectures do not come with instructions saying whether they they should be proven or, instead, refuted. Yet, as we now know, in either case the final argument produced had better be not just convincing but actually verifiable in…
The Agora system is a prototypical Wiki for formal mathematics: a web-based system for collaborating on formal mathematics, intended to support informal documentation of formal developments. This system requires a reusable proof editor…
The generality and pervasiness of category theory in modern mathematics makes it a frequent and useful target of formalization. It is however quite challenging to formalize, for a variety of reasons. Agda currently (i.e. in 2020) does not…
The book "A Course in Constructive Algebra" (1988) shows the way of understanding classical basic algebra in a constructive style similar to Bishop's Constructive Mathematics. Classical theorems are revisited, with a new flavour, and become…
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…
As the development of formal proofs is a time-consuming task, it is important to devise ways of sharing the already written proofs to prevent wasting time redoing them. One of the challenges in this domain is to translate proofs written in…
The main goal of this project is to prove the equivalency of several characterizations of completeness of Archimedean ordered fields; some of which appear in most modern literature as theorems following from the Dedekind completeness of the…
The formal analysis of automated systems is an important and growing industry. This activity routinely requires new verification frameworks to be developed to tackle new programming features, or new considerations (bugs of interest). Often,…
We present axioms for the real numbers by omitting the field axioms and then derive the field properties of the real numbers. We prove all our theorems constructively.
We report about significant enhancements of the complex algebraic geometry theorem proving subsystem in GeoGebra for automated proofs in Euclidean geometry, concerning the extension of numerous GeoGebra tools with proof capabilities. As a…
The Agda Universal Algebra Library (UALib) is a library of types and programs (theorems and proofs) we developed to formalize the foundations of universal algebra in dependent type theory using the Agda programming language and proof…
Abstract interpreters are complex pieces of software: even if the abstract interpretation theory and companion algorithms are well understood, their implementations are subject to bugs, that might question the soundness of their…
In this memoir, we seek to construct a constructive theory that is as complete as possible to describe the algebraic properties of the real number field in constructive mathematics without a dependent choice axiom. To this purpose, we use a…
Modern separation logics allow one to prove rich properties of intricate code, e.g. functional correctness and linearizability of non-blocking concurrent code. However, this expressiveness leads to a complexity that makes these logics…
Exact representations of real numbers such as the signed digit representation or more generally linear fractional representations or the infinite Gray code represent real numbers as infinite streams of digits. In earlier work by the first…
Proof assistants are getting more widespread use in research and industry to provide certified and independently checkable guarantees about theories, designs, systems and implementations. However, proof assistant implementations themselves…
Diproche ("Didactical Proof Checking") is an automatic system for supporting the acquistion of elementary proving skills in the initial phase of university education in mathematics. A key feature of Diproche - which is designed by the…
Software artifacts are ubiquitous in our lives being an essential part of home appliances, cars, cel phones, and even in more critical activities like aeronautics and health sciences. In this context software failures may produce enormous…
To ensure decidability and consistency of its type theory, a proof assistant should only accept terminating recursive functions and productive corecursive functions. Most proof assistants enforce this through syntactic conditions, which can…
Noisy data, non-convex objectives, model misspecification, and numerical instability can all cause undesired behaviors in machine learning systems. As a result, detecting actual implementation errors can be extremely difficult. We…