47 datasets found

This document introduces DBGen, an automatic generator of De Bruijn infrastructure for the Coq proof assistant.

National audience

CertiCrypt is a framework that enables the machine-checked construction and verification of cryptographic proofs in the Coq proof assistant. CertiCrypt instruments the...

C++ is one of the most widely used programming languages in practice, including for embedded critical software. Thus, it becomes interesting to apply formal methods to...

International audience

Last version published in the proceedings of IJCAR 06, part of FLOC 06.

Proof assistants offer a formal framework for formalizing and mechanically checking mathematical knowledge. Moreover, due to the numerous applications that follow from...

Coq is a proof assistant based on a higher-order logic. Coq allows to handle calculus mathematical assertions and to check mechanically proofs of these assertions. It...

Projet COQ

These are course notes on programming language formal descriptions and their use to build programming environments and to prove properties of these languages.

CTCOQ is a graphical environment to perform proofs in Coq.

Projet COQ

Projet COQ

Proof Carrying Code (PCC) is a technique for downloading mobile code on a host machine while ensuring that the code adheres to the host's security policy. We show how...

This paper presents a simple way of performing polynomial simplifications in a proof assistant. This method has been implemented and tested within the Coq prover.

International audience

This thesis focuses on the adaptation of realizability and parametricity to dependent types in the framework of Pure Type Systems. We describe a systematic method to...

Projet GALLIUM

International audience

International audience