Arity-generic datatype-generic programming: (abstract only). - Stephanie Weirich; Chris Casinghino (ACM SIGPLAN Notices, 2009)

Arity-generic datatype-generic programming. - Stephanie Weirich; Chris Casinghino (PLPV, 2010)

Generic Programming with Dependent Types. - Stephanie Weirich; Chris Casinghino (SSGIP, 2010)

Equational reasoning about programs with general recursion and call-by-value semantics. - Garrin Kimmell; Aaron Stump; Harley D. Eades III; Peng Fu 001; Tim Sheard; Stephanie Weirich; Chris Casinghino; Vilhelm Sjöberg; Nathan Collins; Ki Yung Ahn (PLPV, 2012)

Step-Indexed Normalization for a Language with General Recursion - Chris Casinghino; Vilhelm Sjöberg; Stephanie Weirich (MSFP, 2012)

Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems - Vilhelm Sjöberg; Chris Casinghino; Ki Yung Ahn; Nathan Collins; Harley D. Eades III; Peng Fu 001; Garrin Kimmell; Tim Sheard; Aaron Stump; Stephanie Weirich (MSFP, 2012)

Combining proofs and programs in a dependently typed language. - Chris Casinghino; Vilhelm Sjöberg; Stephanie Weirich (POPL, 2014)

specgen: A Tool for Modeling Statecharts in CSP. - Brandon Shapiro; Chris Casinghino (NFM, 2017)

A Verified LL(1) Parser Generator. - Sam Lasser; Chris Casinghino; Kathleen Fisher; Cody Roux (ITP, 2019)

Using Binary Analysis Frameworks: The Case for BAP and angr. - Chris Casinghino; J. T. Paasch; Cody Roux; John Altidor; Michael Dixon; Dustin Jamner (NFM, 2019)

CoStar: a verified ALL(*) parser. - Sam Lasser; Chris Casinghino; Kathleen Fisher; Cody Roux (PLDI, 2021)

Strong Normalization for the Calculus of Constructions. - Chris Casinghino (CoRR, 2022)

Verified ALL(*) Parsing with Semantic Actions and Dynamic Input Validation. - Sam Lasser; Chris Casinghino; Derek Egolf; Kathleen Fisher; Cody Roux (NFM, 2023)

Data Race Freedom à la Mode. - Aïna Linn Georges; Benjamin Peters; Laila Elbeheiry; Leo White; Stephen Dolan; Richard A. Eisenberg; Chris Casinghino; François Pottier; Derek Dreyer (Proc. ACM Program. Lang., 2025)