rép : Autres

fic : Propositions as Types-Wadler-CACM-2015.pdf

fic : Formalisation en Coq et visualisation d’un cours de géométrie pour le lycée-Guilhot-2015.pdf

fic : Certified Version Of Buchberger's Algorithm-Thery-1998.pdf

fic : Sudoku-in-Coq-Thery-2006.pdf

fic : A Machine-Checked Implementation of Buchberger’s Algorithm-Thery-2001.pdf

fic : A_Survey_of_Symbolic_Execution_Techniques-Baldoni-2016.pdf

fic : An Axiomatization of Linear Temporal Logic in the Calculus of Inductive Constructions-Coupet-Grimal-2002.pdf

fic : Formal verification of a realistic compiler-Leroy-2009.pdf

fic : Proof Pearl - Playing with the Tower of Hanoi Formally-Thery-2021-31.pdf

fic : Formal Verification of an Incremental Garbage Collector-Coupet-Grimal-et-al-2003.pdf

fic : Proof Pearl- Revisiting the Mini-rubik in Coq-Thery-2008.pdf

fic : Verified Programming of Turing Machines in Coq-Forster-2019.pdf

fic : ._Formalisation en Coq et visualisation d’un cours de géométrie pour le lycée-Guilhot-2015.pdf

fic : Verification formelle d’extractions de racines entieres-Bertot-2006.pdf

fic : Utilisation des assistants de preuves pour l’enseignement en L1.pdf

fic : Coq-And-Hardware-Verification-Coupet-Grimal-Jakubiec-1996.pdf

fic : Finding and Understanding Bugs in C Compilers-Yang-et-al-2011.pdf

fic : Coq, assistant de preuve-Blazy-et-al-2017.pdf

fic : Contraction-Free Sequent Calculi for Intuitionistic Logic-Dyckhoff-1992.pdf

fic : Proving Pearl- Knuth’s Algorithm for Prime Numbers-Thery-2003.pdf

fic : On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem-Forster-et-al-2019.pdf

fic : Extraction in Coq- An overview-Letouzey_2008.pdf

fic : Symbolic-execution-as-a-basis-for -termination-analysis -Vidal-2015.pdf