Simulating Large Eliminations in Cedille. - Christa Jenkins; Andrew Marmaduke; Aaron Stump (TYPES, 2021)

Towards Formal Verification of HotStuff-Based Byzantine Fault Tolerant Consensus in Agda. - Harold Carr; Christa Jenkins; Mark Moir; Victor Cacciari Miraldo; Lisandra Silva (NFM, 2022)

An approach to translating Haskell programs to Agda and reasoning about them. - Harold Carr; Christa Jenkins; Mark Moir; Victor Cacciari Miraldo; Lisandra Silva (CoRR, 2022)

Proof Engineering with Predicate Transformer Semantics. - Christa Jenkins; Mark Moir; Harold Carr (CoRR, 2022)

A Type-Based Approach to Divide-and-Conquer Recursion in Coq. - Pedro Abreu; Benjamin Delaware; Alex Hubers; Christa Jenkins; J. Garrett Morris; Aaron Stump (Proc. ACM Program. Lang., 2023)

ARMOR: A Formally Verified Implementation of X.509 Certificate Chain Validation. - Joyanta Debnath; Christa Jenkins; Yuteng Sun; Sze Yiu Chau; Omar Chowdhury (SP, 2024)