Closure Under Alpha-Conversion. - Randy Pollack (TYPES, 1993)

A Constructive Algebraic Hierarchy in Coq. - Herman Geuvers; Randy Pollack; Freek Wiedijk; Jan Zwanenburg (J. Symb. Comput., 2002)

Reasoning About CBV Functional Programs in Isabelle/HOL. - John Longley; Randy Pollack (TPHOLs, 2004)

A Logical Framework with Dependently Typed Records. - Thierry Coquand; Randy Pollack; Makoto Takeyama (Fundam. Informaticae, 2005)

Engineering formal metatheory. - Brian E. Aydemir; Arthur Charguéraud; Benjamin C. Pierce; Randy Pollack; Stephanie Weirich (POPL, 2008)

External and internal syntax of the lambda-calculus. - Masahiko Sato 001; Randy Pollack (J. Symb. Comput., 2010)

Preliminary design of the SAFE platform. - André DeHon; Ben Karel; Thomas F. Knight Jr.; Gregory Malecha; Benoît Montagu; Robin Morisset; Greg Morrisett; Benjamin C. Pierce; Randy Pollack; Sumit Ray; Olin Shivers; Jonathan M. Smith; et al. (PLOS@SOSP, 2011)

Certified Complexity. - R. Armadio; Andrea Asperti; Nicholas Ayache; Brian Campbell 001; Dominic P. Mulligan; Randy Pollack; Yann Régis-Gianas; Claudio Sacerdoti Coen; Ian Stark (FET, 2011)

A Canonical Locally Named Representation of Binding. - Randy Pollack; Masahiko Sato 001; Wilmer Ricciotti (J. Autom. Reason., 2012)

A Theory of Information-Flow Labels. - Benoît Montagu; Benjamin C. Pierce; Randy Pollack (CSF, 2013)

Certified Complexity (CerCo). - Roberto M. Amadio; Nicholas Ayache; François Bobot; Jaap Boender; Brian Campbell 001; Ilias Garnier; Antoine Madet; James McKinna; Dominic P. Mulligan; Mauro Piccolo; Randy Pollack; Yann Régis-Gianas; et al. (FOPARA, 2013)

A verified information-flow architecture. - Arthur Azevedo de Amorim; Nathan Collins; André DeHon; Delphine Demange; Catalin Hritcu; David Pichardie; Benjamin C. Pierce; Randy Pollack; Andrew Tolmach (J. Comput. Secur., 2016)