Semantics-Based Compiling: A Case Study in Type-Directed Partial Evaluation. - Olivier Danvy; René Vestergaard (PLILP, 1996)

Equational Reasoning for Linking with First-Class Primitive Modules. - J. B. Wells; René Vestergaard (ESOP, 2000)

A Formalised First-Order Confluence Proof for the lambda-Calculus Using One-Sorted Variable Names. - René Vestergaard; James Brotherston (RTA, 2001)

Cut rules and explicit substitutions. - René Vestergaard; J. B. Wells (Math. Struct. Comput. Sci., 2001)

The Simple Type Theory of Normalization by Evaluation. - René Vestergaard (WRS, 2001)

The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective). - René Vestergaard; James Brotherston (MERLIN, 2001)

A formalised first-order confluence proof for the -calculus using one-sorted variable names. - René Vestergaard; James Brotherston (Inf. Comput., 2003)

Rewriting Game Theory as a Foundation for State-Based Models of Gene Regulation. - Chafika Chettaoui; Franck Delaplace; Pierre Lescanne; Mun'delanji Vestergaard; René Vestergaard (CMSB, 2006)

A constructive approach to sequential Nash equilibria. - René Vestergaard (Inf. Process. Lett., 2006)

Cascaded Games. - Jittisak Senachak; Mun'delanji Vestergaard; René Vestergaard (AB, 2007)

Proof Pearl: De Bruijn Terms Really Do Work. - Michael Norrish; René Vestergaard (TPHOLs, 2007)

Conversion/Preference Games - Stéphane Le Roux 001; Pierre Lescanne; René Vestergaard (CoRR, 2008)

Formalizing Adequacy: A Case Study for Higher-order Abstract Syntax. - James Cheney; Michael Norrish; René Vestergaard (J. Autom. Reason., 2012)

Proofs of life: molecular-biology reasoning simulates cell behaviors from first principles. - René Vestergaard; Emmanuel Pietriga (CoRR, 2018)