Program Verification by Coinduction. - Brandon M. Moore; Lucas Peña; Grigore Rosu (ESOP, 2018)

Foundations for natural proofs and quantifier instantiation. - Christof Löding; P. Madhusudan; Lucas Peña (Proc. ACM Program. Lang., 2018)

Towards a Verified Model of the Algorand Consensus Protocol in Coq. - Musab A. Alturki; Jing Chen; Victor Luchangco; Brandon M. Moore; Karl Palmskog; Lucas Peña; Grigore Rosu (FM Workshops (1), 2019)

Synthesizing Lemmas for Inductive Reasoning. - Adithya Murali; Lucas Peña; Christof Löding; P. Madhusudan (CoRR, 2020)

Towards a unified proof framework for automated fixpoint reasoning using matching logic. - Xiaohong Chen 002; Minh-Thai Trinh; Nishant Rodrigues; Lucas Peña; Grigore Rosu (Proc. ACM Program. Lang., 2020)

Mechanizing Matching Logic in Coq. - Péter Bereczky; Xiaohong Chen 002; Dániel Horpácsi; Tamás Bálint Mizsei; Lucas Peña; Jan Tusil (FROM, 2022)

Model-guided synthesis of inductive lemmas for FOL with least fixpoints. - Adithya Murali; Lucas Peña; Eion Blanchard; Christof Löding; P. Madhusudan (Proc. ACM Program. Lang., 2022)

A First-order Logic with Frames. - Adithya Murali; Lucas Peña; Christof Löding; P. Madhusudan (ACM Trans. Program. Lang. Syst., 2023)

Complete First-Order Reasoning for Properties of Functional Programs. - Adithya Murali; Lucas Peña; Ranjit Jhala; P. Madhusudan (Proc. ACM Program. Lang., 2023)