Benjamin Werner

Available identifiers

Publication	Date of Publication	Type
Extended quasicontinuum methodology for highly heterogeneous discrete systems	2024-05-10	Paper
Formal Proofs for Nonlinear Optimization	2019-09-18	Paper
Certification of real inequalities: templates and sums of squares	2015-06-19	Paper
Certification of bounds of non-linear functions: the templates method	2013-08-09	Paper
Certification of inequalities involving transcendental functions: combining SDP and max-plus approximation	2013-07-26	Paper
Proof-irrelevant model of CC with predicative induction and judgmental equality	2012-04-02	Paper
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses	2011-11-22	Paper
Importing HOL Light into Coq	2010-09-14	Paper
On the Strength of Proof-Irrelevant Type Theories	2009-03-12	Paper
On the strength of proof-irrelevant type theories	2008-11-13	Paper
Simple Types in Type Theory: Deep and Shallow Encodings	2008-09-02	Paper
Foundations of Software Science and Computation Structures	2007-09-28	Paper
A Computational Approach to Pocklington Certificates in Type Theory	2007-05-02	Paper
Term Rewriting and Applications	2005-11-11	Paper
Proof normalization modulo	2005-02-09	Paper
https://portal.mardi4nfdi.de/entity/Q4435473	2003-11-12	Paper
https://portal.mardi4nfdi.de/entity/Q4944850	2000-09-20	Paper
https://portal.mardi4nfdi.de/entity/Q4246950	1999-12-13	Paper
https://portal.mardi4nfdi.de/entity/Q4364399	1998-04-15	Paper
Synthesis of ML programs in the system Coq	1995-01-12	Paper

This page was built for person: Benjamin Werner