Axiomatic Constructor Classes in Isabelle/HOLCF. - Brian Huffman; John Matthews; Peter White (TPHOLs, 2005)

Countable Ordinals. - Brian Huffman (Arch. Formal Proofs, 2005)

A Purely Definitional Universal Domain. - Brian Huffman (TPHOLs, 2009)

Stream Fusion. - Brian Huffman (Arch. Formal Proofs, 2009)

A New Foundation for Nominal Isabelle. - Brian Huffman; Christian Urban (ITP, 2010)

Free Boolean Algebra. - Brian Huffman (Arch. Formal Proofs, 2010)

Formal verification of monad transformers. - Brian Huffman (ICFP, 2012)

Type Constructor Classes and Monad Transformers. - Brian Huffman (Arch. Formal Proofs, 2012)

Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL. - Brian Huffman; Ondrej Kuncar (CPP, 2013)

Type Classes and Filters for Mathematical Analysis in Isabelle/HOL. - Johannes Hölzl; Fabian Immler; Brian Huffman (ITP, 2013)

Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω 1. - Michael Norrish; Brian Huffman (ITP, 2013)

SAW: the software analysis workbench. - Kyle Carter; Adam Foltzer; Joe Hendrix; Brian Huffman; Aaron Tomb (HILT, 2013)

Certified HLints with Isabelle/HOLCF-Prelude. - Joachim Breitner; Brian Huffman; Neil Mitchell; Christian Sternagel (CoRR, 2013)

Constructing Semantic Models of Programs with the Software Analysis Workbench. - Robert Dockins; Adam Foltzer; Joe Hendrix; Brian Huffman; Dylan McNamee; Aaron Tomb (VSTTE, 2016)

HOLCF-Prelude. - Joachim Breitner; Brian Huffman; Neil Mitchell; Christian Sternagel (Arch. Formal Proofs, 2017)

Continuous Formal Verification of Amazon s2n. - Andrey Chudnov; Nathan Collins; Byron Cook; Joey Dodds; Brian Huffman; Colm MacCárthaigh; Stephen Magill; Eric Mertens; Eric Mullen; Serdar Tasiran; Aaron Tomb; Eddy Westbrook (CAV (2), 2018)

Formal Verification of Flow Equivalence in Desynchronized Designs. - Jennifer Paykin; Brian Huffman; Daniel M. Zimmerman; Peter A. Beerel (ASYNC, 2020)

Verified Cryptographic Code for Everybody. - Brett Boston; Samuel Breese; Joey Dodds; Mike Dodds; Brian Huffman; Adam Petcher; Andrei Stefanescu (CAV (1), 2021)

BASALISC: Flexible Asynchronous Hardware Accelerator for Fully Homomorphic Encryption. - Robin Geelen; Michiel Van Beirendonck; Hilder V. L. Pereira; Brian Huffman; Tynan McAuley; Ben Selfridge; Daniel Wagner 001; Georgios D. Dimou; Ingrid Verbauwhede; Frederik Vercauteren; David W. Archer (IACR Cryptol. ePrint Arch., 2022)

BASALISC: Programmable Hardware Accelerator for BGV Fully Homomorphic Encryption. - Robin Geelen; Michiel Van Beirendonck; Hilder V. L. Pereira; Brian Huffman; Tynan McAuley; Ben Selfridge; Daniel Wagner 001; Georgios D. Dimou; Ingrid Verbauwhede; Frederik Vercauteren; David W. Archer (IACR Trans. Cryptogr. Hardw. Embed. Syst., 2023)

$ mathbf{{ textsc {PyCaliper}}}$: Python-Embedded Infrastructure for RTL Verification and Specification Synthesis. - Adwait Godbole; Brian Huffman; Fangfei Liu; Carlos V. Rozas; Sanjit A. Seshia (CAV (3), 2025)