Related papers: A formalization of convex polyhedra based on the s…
Faces play a central role in the combinatorial and computational aspects of polyhedra. In this paper, we present the first formalization of faces of polyhedra in the proof assistant Coq. This builds on the formalization of a library…
Convex polyhedra are the basis for several abstractions used in static analysis and computer-aided verification of complex and sometimes mission critical systems. For such applications, the identification of an appropriate…
The algebraic properties of the combination of probabilistic choice and nondeterministic choice have long been a research topic in program semantics. This paper explains a formalization in the Coq proof assistant of a monad equipped with…
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…
The article deals with operations defined on convex polyhedra or polyhedral convex functions. Given two convex polyhedra, operations like Minkowski sum, intersection and closed convex hull of the union are considered. Basic operations for…
The use of Cauchy's method to prove Euler's well-known formula is an object of many controversies. The purpose of this paper is to prove that Cauchy's method applies for convex polyhedra and not only for them, but also for surfaces such as…
Proving that a finitely generated convex cone is closed is often considered the most difficult part of geometric proofs of Farkas' lemma. We provide a short simple proof of this fact and (for completeness) derive Farkas' lemma from it using…
In the present work, we consider Zuckerberg's method for geometric convex-hull proofs introduced in [Geometric proofs for convex hull defining formulations, Operations Research Letters 44(5), 625-629 (2016)]. It has only been scarcely…
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…
Choreographic programming is a paradigm for writing coordination plans for distributed systems from a global point of view, from which correct-by-construction decentralised implementations can be generated automatically. Theory of…
We give a short survey on computational techniques which can be used to solve the representation conversion problem for polyhedra up to symmetries. We in particular discuss decomposition methods, which reduce the problem to a number of…
The use of Cauchy's method in proving the well-known Euler formula is an object of many controversies. The purpose of this paper is to prove that the Cauchy's method applies for convex polyhedra and not only for them, but also for surfaces…
This paper describes a formalization of discrete real closed fields in the Coq proof assistant. This abstract structure captures for instance the theory of real algebraic numbers, a decidable subset of real numbers with good algorithmic…
This article describes a method to compute successive convex approximations of the convex hull of a set of points in R^n that are the solutions to a system of polynomial equations over the reals. The method relies on sums of squares of…
A programming tactic involving polyhedra is reported that has been widely applied in the polyhedral analysis of (constraint) logic programs. The method enables the computations of convex hulls that are required for polyhedral analysis to be…
We study induction on the program structure as a proof method for bisimulation-based compiler correctness. We consider a first-order language with mutually recursive function definitions, system calls, and an environment semantics. The…
Mathematics formalisation is the task of writing mathematics (i.e., definitions, theorem statements, proofs) in natural language, as found in books and papers, into a formal language that can then be checked for correctness by a program. It…
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…
One can perform equational reasoning about computational effects with a purely functional programming language thanks to monads. Even though equational reasoning for effectful programs is desirable, it is not yet mainstream. This is partly…
We present an approach to constrained Horn clause (CHC) verification combining three techniques: abstract interpretation over a domain of convex polyhedra, specialisation of the constraints in CHCs using abstract interpretation of…