Automatic Proofs of Theorems in Analysis Using Nonstandard Techniques. - A. Michael Ballantyne; W. W. Bledsoe (J. ACM, 1977)

The Metatheorist: Automatic Proofs of Theorems in Analysis Using Non-Standard Techniques, Part II. - A. Michael Ballantyne (Automated Reasoning: Essays in Honor of Woody Bledsoe, 1991)

Recovering user interface specifications for porting transaction processing applications. - Larry Van Sickle; Zheng Yang Liu; Michael Ballantyne (WPC, 1993)

Woody Bledsoe - His Life and Legacy. - A. Michael Ballantyne; Robert S. Boyer; Larry M. Hines (AI Mag., 1996)

Adding interactive visual syntax to textual code. - Leif Andersen; Michael Ballantyne; Matthias Felleisen (Proc. ACM Program. Lang., 2020)

Macros for domain-specific languages. - Michael Ballantyne; Alexis King; Matthias Felleisen (Proc. ACM Program. Lang., 2020)

Dependent type systems as macros. - Stephen Chang 001; Michael Ballantyne; Milo Turner; William J. Bowman (Proc. ACM Program. Lang., 2020)

Injecting Language Workbench Technology into Mainstream Languages. - Michael Ballantyne; Matthias Felleisen (Eelco Visser Commemorative Symposium, 2023)

Compiled, Extensible, Multi-language DSLs (Functional Pearl). - Michael Ballantyne; Mitch Gamburg; Jason Hemann (Proc. ACM Program. Lang., 2024)

Multi-stage Relational Programming. - Michael Ballantyne; Rafaello Sanna; Jason Hemann; William E. Byrd; Nada Amin (Proc. ACM Program. Lang., 2025)