| 2026 | FSCD | Ground Stratified Inductive Definitions. | Nathan Guermond, Gopalan Nadathur |
| 2025 | PPDP | Transporting Theorems about Typeability in LF Across Schematically Defined Contexts. | Chase Johnson, Gopalan Nadathur |
| 2022 | PPDP | A Logic for Formalizing Properties of LF Specifications. | Gopalan Nadathur, Mary Southern |
| 2018 | PPDP | Schematic Polymorphism in the Abella Proof Assistant. | Gopalan Nadathur, Yuting Wang |
| 2016 | ESOP | A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs. | Yuting Wang, Gopalan Nadathur |
| 2013 | PPDP | Reasoning about higher-order relational specifications. | Yuting Wang, Kaustuv Chaudhuri, Andrew Gacek, Gopalan Nadathur |
| 2012 | LICS | Combining Deduction Modulo and Logics of Fixed-Point Definitions. | David Baelde, Gopalan Nadathur |
| 2010 | PPDP | A meta-programming approach to realizing dependently typed logic programming. | Zachary Snow, David Baelde, Gopalan Nadathur |
| 2008 | LICS | Combining Generic Judgments with Recursive Definitions. | Andrew Gacek, Dale Miller, Gopalan Nadathur |
| 2007 | CADE | The Bedwyr System for Model Checking over Syntactic Expressions. | David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu |
| 2005 | ICLP | Practical Higher-Order Pattern Unification with On-the-Fly Raising. | Gopalan Nadathur, Natalie Linnell |
| 2005 | LPAR | Optimizing the Runtime Processing of Types in Polymorphic Logic Programming Languages. | Gopalan Nadathur, Xiaochu Qi |
| 2003 | PPDP | Explicit substitutions in the reduction of lambda terms. | Gopalan Nadathur, Xiaochu Qi |
| 2001 | FLOPS | The Metalanguage lambda-Prolog and Its Implementation. | Gopalan Nadathur |
| 1999 | CADE | System Description: Teyjus - A Compiler and Abstract Machine Based Implementation of lambda-Prolog. | Gopalan Nadathur, Dustin J. Mitchell |
| 1995 | LICS | Uniform Proofs and Disjunctive Logic Programming (Extended Abstract) | Gopalan Nadathur, Donald W. Loveland |
| 1991 | ICLP | Implementation Techniques for Scoping Constructs in Logic Programming. | Bharat Jayaraman, Gopalan Nadathur |
| 1988 | CADE | Lambda-Prolog: An Extended Logic Programming Language. | Amy P. Felty, Elsa L. Gunter, John Hannan, Dale Miller, Gopalan Nadathur, Andre Scedrov |
| 1988 | ICLP | An Overview of Lambda-PROLOG. | Gopalan Nadathur, Dale Miller |
| 1987 | LICS | Hereditary Harrop Formulas and Uniform Proof Systems | Dale Miller, Gopalan Nadathur, Andre Scedrov |
| 1986 | ACL | Some Uses of Higher-Order Logic in Computational Linguistics. | Dale Miller, Gopalan Nadathur |
| 1986 | ICLP | Higher-Order Logic Programming. | Dale Miller, Gopalan Nadathur |
| 1983 | IJCAI | Mutual Beliefs in Conversational Systems: Their Role in Referring Expressions. | Gopalan Nadathur, Aravind K. Joshi |