-
A list-machine benchmark for mechanized metatheory
Projet GALLIUM -
Formal Verification of Hardware Synthesis
International audience -
Matrices à blocs et en forme canonique
International audience -
Une Analyse Formelle en Coq d'un Algorithme Distribué Probabiliste résolvant ...
International audience -
Un régime au concentré d'automate
International audience -
Formalized algebraic numbers: construction and first-order theory.
This thesis presents a formalization of algebraic numbers and their theory. It brings two new important contributions to the formalization of mathematical results in... -
Certification of a Tool Chain for Deductive Program Verification
This thesis belongs to the domain of software verification. The goalof verifying software is to ensure that an implementation, a program,satisfies the requirements,... -
From Tarski to Hilbert
International audience -
Point-Free, Set-Free Concrete Linear Algebra
International audience -
Efficient Generation of Correctness Certificates for the Abstract Domain of P...
International audience -
Extracting Herbrand trees from Coq
Software certification aims at proving the correctness of programs but in many cases, the use of external libraries allows only a conditional proof: it depends on the... -
Implementing hash-consed structures in Coq
International audience -
Simple simpl
We report on a new implementation of a reduction strategy in Coq to simplify terms during interactive proofs. By "simplify", we mean to reduce terms as much as... -
Proof Automation for Atelier B Rules Verification
The purpose of this thesis is the verification of Atelier B added rules using the framework named BCARe which relies on a deep embedding of the B theory within the... -
Common Knowledge Logic in a Higher Order Proof Assistant
This paper presents experiments on common knowledge logic, conducted with the help of the proof assistant Coq. The main feature of common knowledge logic is the... -
Implementation of three types of ordinals in Coq
One can define an inductive type T in Coq by the rules: zero is in T, and 'cons a n b' is in T when a, b are in T and n is an integer. One can embed this type with an... -
Development and verification of probability logics and logical frameworks
We introduce a Probability Logic with Conditional Operators - LPCP, its syntax, semantics, and a sound and strongly-complete axiomatic system, featuring an infinitary... -
CoLoR: a Coq library on rewriting and termination
International audience -
Handcrafted Inversions Made Operational on Operational Semantics
International audience
