Empreinte digitale
- 1 Profils similaires
Collaborations et principaux domaines de recherche des cinq dernières années
Résultat de recherche
-
A drag-and-drop proof tactic
Donato, P., Strub, P. Y. & Werner, B., 11 janv. 2022, CPP 2022 - Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2022. Popescu, A. & Zdancewic, S. (eds.). Association for Computing Machinery, Inc, p. 197-209 13 p. (CPP 2022 - Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2022).Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs
Accès ouvert -
Certification of real inequalities: templates and sums of squares
Magron, V., Allamigeon, X., Gaubert, S. & Werner, B., 12 nov. 2015, Dans: Mathematical Programming. 151, 2, p. 477-506 30 p.Résultats de recherche: Contribution à un journal › Article › Revue par des pairs
Accès ouvert -
Formal proofs for nonlinear optimization
Magron, V., Allamigeon, X., Gaubert, S. & Werner, B., 1 janv. 2015, Dans: Journal of Formalized Reasoning. 8, 1, p. 1-24 24 p.Résultats de recherche: Contribution à un journal › Article › Revue par des pairs
-
Certification of inequalities involving transcendental functions: Combining SDP and max-plus approximation
Allamigeon, X., Gaubert, S., Magron, V. & Werner, B., 1 janv. 2013, 2013 European Control Conference, ECC 2013. IEEE Computer Society, p. 2244-2250 7 p. 6669514. (2013 European Control Conference, ECC 2013).Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs
Accès ouvert -
The templates method
Allamigeon, X., Gaubert, S., Magron, V. & Werner, B., 1 août 2013, Intelligent Computer Mathematics - MKM, Calculemus, DML, and Systems and Projects 2013 - Held as Part of CICM 2013, Proceedings. p. 51-65 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol 7961 LNAI).Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs
Accès ouvert -
A modular integration of SAT/SMT solvers to Coq through proof witnesses
Armand, M., Faure, G., Grégoire, B., Keller, C., Théry, L. & Werner, B., 1 janv. 2011, Certified Programs and Proofs - First International Conference, CPP 2011, Proceedings. Springer Verlag, p. 135-150 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol 7086 LNCS).Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs
Accès ouvert -
Proof-irrelevant model of CC with predicative induction and judgmental equality
Gyesik, L. & Werner, B., 1 janv. 2011, Dans: Logical Methods in Computer Science. 7, 4, p. 1-25 25 p.Résultats de recherche: Contribution à un journal › Article › Revue par des pairs
-
Importing HOL light into Coq
Keller, C. & Werner, B., 1 janv. 2010, Interactive Theorem Proving - First International Conference, ITP 2010, Proceedings. Springer Verlag, p. 307-322 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol 6172 LNCS).Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs
Accès ouvert -
On the strength of proof-irrelevant type theories
Werner, B., 26 sept. 2008, Dans: Logical Methods in Computer Science. 4, 3, 13.Résultats de recherche: Contribution à un journal › Article › Revue par des pairs
Accès ouvert -
Simple types in type theory: Deep and shallow encodings
Garillot, F. & Werner, B., 1 janv. 2007, Theorem Proving in Higher Order Logics - 20th International Conference, TPHOLs 2007, Proceedings. Springer Verlag, p. 368-382 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol 4732 LNCS).Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs