-
Proofs with Coq of theorems in plane geometry using oriented angles
Formalization of the theory of oriented angles of non zero vectors using Coq is reported. Using this theory, some classical plane geometry theorems are proved, among... -
Proofs with Coq of theorems in plane geometry using oriented angles
Formalization of the theory of oriented angles of non zero vectors using Coq is reported. Using this theory, some classical plane geometry theorems are proved, among... -
Mathematics and Proof Presentation in Pcoq
We present PCOQ , a user-interface for the Coq system which provides elaborate mathematical formulas lay-out.We first show how the organization of thegraphic- al... -
Reflecting BDDs in Coq
Projet COQ -
A study on the relationship between knowledge and proof: the case of the noti...
This research presents an analysis of the relationship between knowledge and proof through a mathematical concept: reflective symmetry (in a situation of construction... -
Programming Language Specifications and Environments
These are course notes on programming language formal descriptions and their use to build programming environments and to prove properties of these languages. -
Toward convergence of the variational mass expansion in asymptotically free t...
We re-examine a modification of perturbative expansions, valid for asymptotically free theories, producing "variationally improved" expansions of physical quantities... -
La logique à la croisée des chemins : la controverse Goblot-Rougier sur la na...
International audience -
CoLoR: a Coq library on rewriting and termination
International audience -
Formal and Incremental Construction of Distributed Algorithms: On the Distrib...
The development of distributed algorithms and, more generally, distributed systems, is a complex, delicate and challenging process. Refinement techniques of (system)... -
Proving dynamic properties in B
The properties that we would like to express on data-intensive applications cannot be limited to static properties, called invariance properties, which depend on... -
Modeling of the defining activity in mathematics and of its dialectic with th...
This text proposes an epistemological modeling of the mathematical defining activity, and highlights the links between defining and proving. The goals are also... -
Event-B based approach for verifying dynamic composite service transactional ...
International audience -
Parallélisation d'une simulation Monte Carlo d'un système de spins et preuve
Colloque avec actes et comité de lecture. -
Formal engineering of the bitonic sort using pvs
Colloque avec actes et comité de lecture.
