Passer à la navigation principale Passer à la recherche Passer au contenu principal
1993 …2022

Résultat de recherche par an

Empreinte digitale

Passez en revue plus en détail les thèmes de recherche où Benjamin Werner est actif. Ces libellés thématiques proviennent des travaux de cette personne. Ensemble, ils forment une empreinte digitale unique.
  • 1 Profils similaires

Collaborations et principaux domaines de recherche des cinq dernières années

Collaboration externe récente au niveau du pays/territoire. Voir les détails en cliquant sur les points ou
  • 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 collectionContribution à une conférenceRevue 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 journalArticleRevue 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 journalArticleRevue 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 collectionContribution à une conférenceRevue 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 collectionContribution à une conférenceRevue 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 collectionContribution à une conférenceRevue 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 journalArticleRevue 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 collectionContribution à une conférenceRevue 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 journalArticleRevue 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 collectionContribution à une conférenceRevue par des pairs