The Handbook of Geometric Constraint Systems Principles is an entry point to the currently
used principal mathematical and computational tools and techniques of the geometric …

In this article, we show how one can formalise in type theory mathematical objects, for which
dependent types are usually deemed unavoidable, using only simple types. We outline a …

We study two different descriptions of incidence projective geometry: a synthetic,
mathematics-oriented one and a more practical, computation-oriented one, based on the …

In this paper, we report on the formalization of a synthetic proof of Pappus' theorem. We
provide two versions of the theorem: the first one is proved in neutral geometry (without …

We present a formalization of Projective Geometry in the proof assistant and programming
language Agda. We formalize a recent development in constructive Projective Geometry …

This thesis applies formal verification to the running time analysis of algorithms. First, three
Hoare logics for time bounds from the literature are studied and their application to …

We present an automatic theorem prover for projective incidence geometry. This prover
does not consider coordinates. Instead, it follows a combinatorial approach based on the …

Mechanizing proofs of geometric theorems in 3D is significantly more challenging than in
2D. As a first noteworthy case study, we consider an iconic theorem of 3D geometry …

Several tools have been developed to enhance automation of theorem proving in the 2D
plane. However, in 3D, only a few approaches have been studied, and to our knowledge …

We describe formalization of the Poincaré disc model of hyperbolic geometry within the
Isabelle/HOL proof assistant. The model is defined within the complex projective line CP^ 1 …