1682849792013-03-252024-03-14T05:43:06The Coq proof assistant - http://coq.inria.fr (2013-07-01)Interactive theorem proving and program development / Y. Bertot, P. Castéran, 200416694325
Coq (logiciel)Coq (logiciel)Assistants de preuveDifferential program semantics / Thibaut Girka ; sous la direction de Roberto Di Cosmo et de David Mentré / , 2018Approche combinatoire pour l'automatisation en Coq des preuves formelles en géométrie d'incidence projective / David Braun ; sous la direction de Pascal Schreck / , 2020Une étude formelle de la théorie des calculs locaux à l'aide de l'assistant de preuve Coq / Vincent Filou ; sous la direction de Pierre Castéran et de Mohamed Mosbah / , 2012Formalisations en Coq pour la décision de problèmes en géométrie algébrique réelle / Boris Djalal ; sous la direction de Yves Bertot / , 2018Verasco : a Formally Verified C Static Analyzer / Jacques-Henri Jourdan ; sous la direction de Xavier Leroy / [Lieu de publication inconnu] : [éditeur inconnu] , 2016Méthodes pour la vérification des protocoles cryptographiques dans le modèle calculatoire / Mathilde Duclos ; sous la direction de Yassine Lakhnech et de Pierre Corbineau / , 2016Challenges in the collaborative evolution of a proof language and its ecosystem / Théo Zimmermann ; sous la direction de Hugo Herbelin et de Yann Régis-Gianas / , 2019Interactive theorem proving and program development : Coq'Art : the calculus of inductive constructions / Yves Bertot, Pierre Castéran ; foreword by Gérard Huet and Christine Paulin-Mohring / Berlin : SpringerProgrammation impérative par raffinements avec l'assistant de preuve Coq / Boubacar Demba Sall ; sous la direction de Emmanuel Chailloux et de Frédéric Peschanski / , 2020Vérification formelle de programmes de génération de données structurées / Richard Genestier ; sous la direction de Olga Kouchnarenko et de Alain Giorgetti / , 2016Développement et vérification des logiques probabilistes et des cadres logiques / Petar Maksimović ; sous la direction de Luigi Liquori et de Silvia Ghilezan / , 2013De nouveaux outils pour calculer avec des inductifs en Coq / Pierre Boutillier ; sous la direction de Hugo Herbelin / Lille : Atelier national de reproduction des thèses , 2014Formalisation en Coq des algorithmes de filtre numérique calculés en précision finie / Diane Gallois-Wong ; sous la direction de Sylvie Boldo et de Thibault Hilaire / , 2021Formalisation des nombres algébriques : construction et théorie du premier ordre / par Cyril Cohen ; sous la direction de Assia Mahboubi / [S.l.] : [s.n.] , 2012Formalisation and Meta-Theory of Type Theory / Théo Winterhalter ; sous la direction de Nicolas Tabareau et de Matthieu Sozeau / , 2020Interactive theorem proving and program development : Coq'Art : the calculus of inductive constructions / Yves Bertot, Pierre Castéran ; foreword by Gérard Huet and Christine Paulin-Mohring / Berlin : SpringerDe nouveaux outils pour calculer avec des inductifs en Coq / Pierre Boutillier ; sous la direction de Hugo Herbelin / [S.l.] : [s.n.] , 2014Effectful programs and their proofs in type theory : application to certified compilation and certified packet processing / Pierre Nigron ; sous la direction de Julia Lawall et de Pierre-Evariste Dagand / , 2022Compilation formellement vérifiée de code C de bas-niveau / Pierre Wilke ; sous la direction de Sandrine Blazy et de Frédéric Besson / , 2016A formalization of elliptic curves for cryptography / Evmorfia-Iro Bartzia ; sous la direction de Karthikeyan Bhargavan / , 2017Étude formelle d'algorithmes efficaces en algèbre linéaire / Maxime Dénès ; sous la direction de Yves Bertot / , 2013Repenser la bibliothèque réelle de Coq : vers une formalisation de l'analyse classique mieux adaptée / Catherine Lelay ; sous la direction de Sylvie Boldo et de Guillaume Melquiond / , 2015Le co-design d'un noyau de système d'exploitation et de sa preuve formelle d'isolation / Narjes Jomaa ; sous la direction de Gilles Grimaud et de David Nowak / , 2018De nouveaux outils pour calculer avec des inductifs en Coq / Pierre Boutillier / Villeurbanne : [CCSD] , 2014Verasco : a Formally Verified C Static Analyzer / Jacques-Henri Jourdan ; sous la direction de Xavier Leroy / Lille : Atelier national de reproduction des thèses , 2016Analyse de dépendances ML pour les évaluateurs de logiciels critiques. / Vincent Benayoun ; sous la direction de Catherine Dubois / , 2014Computer arithmetic and formal proofs : verifying floating-point algorithms with the Coq system / Sylvie Boldo, Guillaume Melquiond / London : ISTE Press , 2017Lawvere-Tierney sheafification in Homotopy Type Theory / Kevin Quirin ; sous la direction de Nicolas Tabareau / , 2016Formalisation des nombres algébriques [Ressource électronique] : construction et théorie du premier ordre / par Cyril Cohen ; sous la direction de Assia Mahboubi / Villeurbanne : TEL , 2013Traduction mécanisée et certifiée en Coq d'une algèbre relationnelle étendue pour SQL vers une algèbre imbriquée / Mohammed Houssem Eddine Hachmaoui ; sous la direction de Evelyne Contejean et de Véronique Benzaken / , 2020Support mécanisé pour la spécification formelle, la vérification et le déploiement d'applications à base de composants / Nuno Gaspar ; sous la direction de Éric Madelaine et de Ludovic Henrio / , 2014Certified programming with dependent types : a pragmatic introduction to the Coq proof assistant / Adam Chlipala / Cambridge (Mass.) : The MIT Press , cop. 2013Bibliothèque certifiée en Coq pour la provenance des données / Rébecca Zucchini ; sous la direction de Véronique Benzaken et de Sarah Cohen-Boulakia et de Chantal Keller / , 2023Formalisation des nombres algébriques : construction et théorie du premier ordre / par Cyril Cohen ; sous la direction de Assia Mahboubi / Lille : Atelier national de reproduction des thèses , 2012Extraction de code fonctionnel certifié à partir de spécifications inductives / Pierre-Nicolas Tollitte ; sous la direction de Catherine Dubois et de David Delahaye / , 2013Vérification formelle de programmes de génération de données structurées / Richard Genestier ; sous la direction de Olga Kouchnarenko et de Alain Giorgetti / , 2016Computer arithmetic and formal proofs : verifying floating-point algorithms with the Coq system / Sylvie Boldo, Guillaume Melquiond / London : ISTE Press , 2017Support mécanisé pour la spécification formelle, la vérification et le déploiement d'applications à base de composants / Nuno Gaspar le 2014 [ Nice ] Extraction de code fonctionnel certifié à partir de spécifications inductives / Pierre-Nicolas Tollitte le 2013 [ Paris, CNAM ] Repenser la bibliothèque réelle de Coq : vers une formalisation de l'analyse classique mieux adaptée / Catherine Lelay le 2015 [ Paris 11 ] Formalisation and Meta-Theory of Type Theory / Théo Winterhalter le 2020 [ Nantes ] Formalisation des nombres algébriques : construction et théorie du premier ordre / Cyril Cohen le 2012 [ Palaiseau, Ecole polytechnique ] Compilation formellement vérifiée de code C de bas-niveau / Pierre Wilke le 2016 [ Rennes 1 ] Differential program semantics / Thibaut Girka le 2018 [ Sorbonne Paris Cité ] Lawvere-Tierney sheafification in Homotopy Type Theory / Kevin Quirin le 2016 [ Nantes, Ecole des Mines ] Analyse de dépendances ML pour les évaluateurs de logiciels critiques. / Vincent Benayoun le 2014 [ Paris, CNAM ] Vérification formelle de programmes de génération de données structurées / Richard Genestier le 2016 [ Besançon ] Étude formelle d'algorithmes efficaces en algèbre linéaire / Maxime Dénès le 2013 [ Nice ] Développement et vérification des logiques probabilistes et des cadres logiques / Petar Maksimović le 2013 [ Nice ] Programmation impérative par raffinements avec l'assistant de preuve Coq / Boubacar Demba Sall le 2020 [ Sorbonne université ] Traduction mécanisée et certifiée en Coq d'une algèbre relationnelle étendue pour SQL vers une algèbre imbriquée / Mohammed Houssem Eddine Hachmaoui le 2020 [ université Paris-Saclay ] Effectful programs and their proofs in type theory : application to certified compilation and certified packet processing / Pierre Nigron le 2022 [ Sorbonne université ] Challenges in the collaborative evolution of a proof language and its ecosystem / Théo Zimmermann le 2019 [ Université Paris Cité ] De nouveaux outils pour calculer avec des inductifs en Coq / Pierre Boutillier le 2014 [ Paris 7 ] A formalization of elliptic curves for cryptography / Evmorfia-Iro Bartzia le 2017 [ Université Paris-Saclay (ComUE) ] Approche combinatoire pour l'automatisation en Coq des preuves formelles en géométrie d'incidence projective / David Braun le 2019 [ Strasbourg ] Verasco : a Formally Verified C Static Analyzer / Jacques-Henri Jourdan le 2016 [ Sorbonne Paris Cité ] Bibliothèque certifiée en Coq pour la provenance des données / Rébecca Zucchini le 2023 [ université Paris-Saclay ] Formalisation en Coq des algorithmes de filtre numérique calculés en précision finie / Diane Gallois-Wong le 2021 [ université Paris-Saclay ] Méthodes pour la vérification des protocoles cryptographiques dans le modèle calculatoire / Mathilde Duclos le 2016 [ Université Grenoble Alpes (ComUE) ] Le co-design d’un noyau de système d’exploitation et de sa preuve formelle d’isolation / Narjes Jomaa le 2018 [ Université de Lille (2018-2021) ] Une étude formelle de la théorie des calculs locaux à l'aide de l'assistant de preuve Coq / Vincent Filou le 2012 [ Bordeaux 1 ] Formalisations en Coq pour la décision de problèmes en géométrie algébrique réelle / Boris Djalal le 2018 [ Université Côte d'Azur (ComUE) ]