Fingerprint
- 1 Similar Profiles
Collaborations and top research areas from the last five years
-
A drag-and-drop proof tactic
Donato, P., Strub, P. Y. & Werner, B., 11 Jan 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).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review
Open Access -
Certification of real inequalities: templates and sums of squares
Magron, V., Allamigeon, X., Gaubert, S. & Werner, B., 12 Nov 2015, In: Mathematical Programming. 151, 2, p. 477-506 30 p.Research output: Contribution to journal › Article › peer-review
Open Access -
Formal proofs for nonlinear optimization
Magron, V., Allamigeon, X., Gaubert, S. & Werner, B., 1 Jan 2015, In: Journal of Formalized Reasoning. 8, 1, p. 1-24 24 p.Research output: Contribution to journal › Article › peer-review
-
Certification of inequalities involving transcendental functions: Combining SDP and max-plus approximation
Allamigeon, X., Gaubert, S., Magron, V. & Werner, B., 1 Jan 2013, 2013 European Control Conference, ECC 2013. IEEE Computer Society, p. 2244-2250 7 p. 6669514. (2013 European Control Conference, ECC 2013).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review
Open Access -
The templates method
Allamigeon, X., Gaubert, S., Magron, V. & Werner, B., 1 Aug 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).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review
Open Access -
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 Jan 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).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review
Open Access -
Proof-irrelevant model of CC with predicative induction and judgmental equality
Gyesik, L. & Werner, B., 1 Jan 2011, In: Logical Methods in Computer Science. 7, 4, p. 1-25 25 p.Research output: Contribution to journal › Article › peer-review
-
Importing HOL light into Coq
Keller, C. & Werner, B., 1 Jan 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).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review
-
On the strength of proof-irrelevant type theories
Werner, B., 26 Sept 2008, In: Logical Methods in Computer Science. 4, 3, 13.Research output: Contribution to journal › Article › peer-review
Open Access -
Simple types in type theory: Deep and shallow encodings
Garillot, F. & Werner, B., 1 Jan 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).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review