Skip to main navigation Skip to search Skip to main content
No photo of Benjamin Werner

View Scopus Profile

Benjamin Werner

Associate Professor

  • 526
    Citations
1993 …2022

Research activity per year

Fingerprint

Dive into the research topics where Benjamin Werner is active. These topic labels come from the works of this person. Together they form a unique fingerprint.
  • 1 Similar Profiles
View full fingerprint

Collaborations and top research areas from the last five years

Recent external collaboration on country/territory level. Dive into details by clicking on the dots or
Explore network further

  • 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
    8 Citations (Scopus)

  • 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
    2 Citations (Scopus)

  • 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

    18 Citations (Scopus)

  • 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
    6 Citations (Scopus)

  • 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
    1 Citation (Scopus)

  • 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
    110 Citations (Scopus)

  • 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

    9 Citations (Scopus)

  • 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

    Open Access
    35 Citations (Scopus)

  • 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
    18 Citations (Scopus)

  • 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

    12 Citations (Scopus)
View all 22 research outputs