Synthesis of ML Programs in the System Coq. - Christine Paulin-Mohring; Benjamin Werner (J. Symb. Comput., 1993)

On the Church-Rosser Property for Expressive Type Systems and its Consequences for their Metatheoretic Study - Herman Geuvers; Benjamin Werner (LICS, 1994)

Une Théorie des Constructions Inductives. - Benjamin Werner (1994)

A Generic Normalisation Proof for Pure Type Systems. - Paul-André Melliès; Benjamin Werner (TYPES, 1996)

Sets in Types, Types in Sets. - Benjamin Werner (TACS, 1997)

The Not So Simple Proof-Irrelevant Model of CC. - Alexandre Miquel; Benjamin Werner (TYPES, 2002)

Proof normalization modulo. - Gilles Dowek; Benjamin Werner (J. Symb. Log., 2003)

Choice in Dynamic Linking. - Martín Abadi; Georges Gonthier; Benjamin Werner (FoSSaCS, 2004)

Arithmetic as a Theory Modulo. - Gilles Dowek; Benjamin Werner (RTA, 2005)

A Computational Approach to Pocklington Certificates in Type Theory. - Benjamin Grégoire; Laurent Théry; Benjamin Werner (FLOPS, 2006)

Simple Types in Type Theory: Deep and Shallow Encodings. - François Garillot; Benjamin Werner (TPHOLs, 2007)

On the Strength of Proof-irrelevant Type Theories. - Benjamin Werner (Log. Methods Comput. Sci., 2008)

Importing HOL Light into Coq. - Chantal Keller; Benjamin Werner (ITP, 2010)

A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. - Michaël Armand; Germain Faure; Benjamin Grégoire; Chantal Keller; Laurent Théry; Benjamin Werner (CPP, 2011)

Using Co-existing Attractors of a Sensorimotor Loop for the Motion Control of a Humanoid Robot. - Matthias Kubisch; Benjamin Werner; Manfred Hild (IJCCI (NCTA), 2011)

Proof-irrelevant model of CC with predicative induction and judgmental equality - Gyesik Lee; Benjamin Werner (Log. Methods Comput. Sci., 2011)

Dynamics of Mutant Cells in Hierarchical Organized Tissues. - Benjamin Werner; David Dingli; Tom Lenaerts; Jorge M. Pacheco; Arne Traulsen (PLoS Comput. Biol., 2011)

Neural Implementation of Behavior Control. - Matthias Kubisch; Christian Benckendorff; Benjamin Werner; Stefan Bethge; Manfred Hild (Language Grounding in Robots, 2012)

Certification of inequalities involving transcendental functions: Combining SDP and max-plus approximation. - Xavier Allamigeon; Stephane Gaubert; Victor Magron; Benjamin Werner (ECC, 2013)

Certification of Bounds of Non-linear Functions: The Templates Method. - Xavier Allamigeon; Stéphane Gaubert; Victor Magron; Benjamin Werner (MKM/Calculemus/DML, 2013)

Formal Proofs for Nonlinear Optimization. - Victor Magron; Xavier Allamigeon; Stéphane Gaubert; Benjamin Werner (J. Formaliz. Reason., 2015)

Certification of real inequalities: templates and sums of squares. - Victor Magron; Xavier Allamigeon; Stéphane Gaubert; Benjamin Werner (Math. Program., 2015)

Variation of mutational burden in healthy human tissues suggests non-random strand segregation and allows measuring somatic mutation rates. - Benjamin Werner; Andrea Sottoriva (PLoS Comput. Biol., 2018)

Spatially constrained tumour growth affects the patterns of clonal selection and neutral drift in cancer genomic data. - Ketevan Chkhaidze; Timon Heide; Benjamin Werner; Marc J. Williams; Weini Huang; Giulio Caravagna; Trevor A. Graham; Andrea Sottoriva (PLoS Comput. Biol., 2019)

A drag-and-drop proof tactic. - Pablo Donato; Pierre-Yves Strub; Benjamin Werner (CPP, 2022)

Proposed V-Model for Verification, Validation, and Safety Activities for Artificial Intelligence. - Benjamin Schumeg; Franklin Marotta; Benjamin Werner (ICAA, 2023)

A constructive proof of Skolem theorem for constructive logic. - Gilles Dowek; Benjamin Werner (CoRR, 2023)

On the Definition of the Eta-long Normal Form in Type Systems of the Cube. - Gilles Dowek; Gérard Huet; Benjamin Werner (CoRR, 2023)