Synthesizable high level hardware descriptions: using statically typed two-level languages to guarantee verilog synthesizability. - Jennifer Gillenwater; Gregory Malecha; Cherif R. Salama; Angela Yun Zhu; Walid Taha; Jim Grundy; John O'Leary (PEPM, 2008)

Effective interactive proofs for higher-order imperative programs. - Adam Chlipala; J. Gregory Malecha; Greg Morrisett; Avraham Shinnar; Ryan Wisnesky (ICFP, 2009)

Mechanized Verification with Sharing. - J. Gregory Malecha; Greg Morrisett (ICTAC, 2010)

A more precise security type system for dynamic security tests. - Gregory Malecha; Stephen Chong (PLAS, 2010)

Toward a verified relational database management system. - J. Gregory Malecha; Greg Morrisett; Avraham Shinnar; Ryan Wisnesky (POPL, 2010)

Synthesizable High Level Hardware Descriptions. - Jennifer Gillenwater; Gregory Malecha; Cherif R. Salama; Angela Yun Zhu; Walid Taha; Jim Grundy; John O'Leary (New Gener. 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)

Trace-based verification of imperative programs with I/O. - Gregory Malecha; Greg Morrisett; Ryan Wisnesky (J. Symb. Comput., 2011)

Static consistency checking for Verilog wire interconnects - Using dependent types to check the sanity of Verilog descriptions. - Cherif R. Salama; Gregory Malecha; Walid Taha; Jim Grundy; John O'Leary (High. Order Symb. Comput., 2011)

Hardware Support for Safety Interlocks and Introspection. - Udit Dhawan; Albert Kwon; Edin Kadric; Catalin Hritcu; Benjamin C. Pierce; Jonathan M. Smith; André DeHon; Gregory Malecha; Greg Morrisett; Thomas F. Knight Jr.; Andrew Sutherland; Tom Hawkins; et al. (SASO Workshops, 2012)

MirrorShard: Proof by Computational Reflection with Verified Hints - Gregory Malecha; Adam Chlipala; Thomas Braibant; Patrick Hulin; Edward Z. Yang (CoRR, 2013)

Compositional Computational Reflection. - Gregory Malecha; Adam Chlipala; Thomas Braibant (ITP, 2014)

Using dependent types and tactics to enable semantic optimization of language-integrated queries. - Gregory Malecha; Ryan Wisnesky (DBPL, 2015)

Towards verification of hybrid systems in a foundational proof assistant. - Daniel Ricketts 001; Gregory Malecha; Mario M. Alvarez; Vignesh Gowda; Sorin Lerner (MEMOCODE, 2015)

Automated software winnowing. - Gregory Malecha; Ashish Gehani; Natarajan Shankar (SAC, 2015)

Towards foundational verification of cyber-physical systems. - Gregory Malecha; Daniel Ricketts 001; Mario M. Alvarez; Sorin Lerner (SOSCYPS@CPSWeek, 2016)

Modular deductive verification of sampled-data systems. - Daniel Ricketts 001; Gregory Malecha; Sorin Lerner (EMSOFT, 2016)

Extensible and Efficient Automation Through Reflective Tactics. - Gregory Malecha; Jesper Bengtson (ESOP, 2016)

Interaction Trees: Representing Recursive and Impure Programs in Coq (Work In Progress). - Li-yao Xia; Yannick Zakowski; Paul He; Chung-Kil Hur; Gregory Malecha; Benjamin C. Pierce; Steve Zdancewic (CoRR, 2019)

The MetaCoq Project. - Matthieu Sozeau; Abhishek Anand; Simon Boulier; Cyril Cohen; Yannick Forster 002; Fabian Kunze; Gregory Malecha; Nicolas Tabareau; Théo Winterhalter (J. Autom. Reason., 2020)

Interaction trees: representing recursive and impure programs in Coq. - Li-yao Xia; Yannick Zakowski; Paul He; Chung-Kil Hur; Gregory Malecha; Benjamin C. Pierce; Steve Zdancewic (Proc. ACM Program. Lang., 2020)

Formal Methods for the Informal Engineer: Workshop Recommendations. - Gopal Sarma; James Koppel; Gregory Malecha; Patrick Schultz; Eric Drexler; Ramana Kumar; Cody Roux; Philip Zucker (CoRR, 2021)

Developing With Formal Methods at BedRock Systems, Inc. - Gregory Malecha; Gordon Stewart 001; Frantisek Farka; Jasper Haag; Yoichi Hirai (IEEE Secur. Priv., 2022)

Modular, Full-System Verification. - Gregory Malecha; Hoang-Hai Dang; Paolo G. Giarrusso; Simon Hudon; Jan-Oliver Kaiser; David Swasey (HotOS, 2025)