| Publication | Date of Publication | Type |
|---|
A quasicontinuum method with optimized local maximum-entropy interpolation and Heaviside enrichment for heterogeneous lattices International Journal for Numerical Methods in Engineering | 2026-08-27 | Paper |
A Quasicontinuum Method with Optimized Local Maximum-Entropy Interpolation and Heaviside Enrichment for Heterogeneous Lattices (available as arXiv preprint) | 2026-01-01 | Paper |
Extended quasicontinuum methodology for highly heterogeneous discrete systems International Journal for Numerical Methods in Engineering | 2024-05-10 | Paper |
Formal Proofs for Nonlinear Optimization (available as arXiv preprint) | 2019-09-18 | Paper |
Certification of real inequalities: templates and sums of squares Mathematical Programming. Series A. Series B | 2015-06-19 | Paper |
Certification of bounds of non-linear functions: the templates method Lecture Notes in Computer Science | 2013-08-09 | Paper |
| Certification of inequalities involving transcendental functions: combining SDP and max-plus approximation | 2013-07-26 | Paper |
Certification of inequalities involving transcendental functions: combining SDP and max-plus approximation (available as arXiv preprint) | 2013-01-01 | Paper |
Proof-irrelevant model of CC with predicative induction and judgmental equality Logical Methods in Computer Science | 2012-04-02 | Paper |
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses Certified Programs and Proofs | 2011-11-22 | Paper |
Importing HOL Light into Coq Interactive Theorem Proving | 2010-09-14 | Paper |
On the Strength of Proof-Irrelevant Type Theories Automated Reasoning | 2009-03-12 | Paper |
On the strength of proof-irrelevant type theories Logical Methods in Computer Science | 2008-11-13 | Paper |
Simple Types in Type Theory: Deep and Shallow Encodings Lecture Notes in Computer Science | 2008-09-02 | Paper |
Foundations of Software Science and Computation Structures Lecture Notes in Computer Science | 2007-09-28 | Paper |
A Computational Approach to Pocklington Certificates in Type Theory Functional and Logic Programming | 2007-05-02 | Paper |
Term Rewriting and Applications Lecture Notes in Computer Science | 2005-11-11 | Paper |
Proof normalization modulo Journal of Symbolic Logic | 2005-02-09 | Paper |
Proof normalization modulo Journal of Symbolic Logic | 2005-02-09 | Paper |
| scientific article; zbMATH DE number 2003160 (Why is no real title available?) | 2003-11-12 | Paper |
Proof normalization modulo Lecture Notes in Computer Science | 2000-09-20 | Paper |
A generic normalisation proof for pure type systems Lecture Notes in Computer Science | 1999-12-13 | Paper |
Sets in types, types in sets Lecture Notes in Computer Science | 1998-04-15 | Paper |
Synthesis of ML programs in the system Coq Journal of Symbolic Computation | 1995-01-12 | Paper |