Mutual Beliefs in Conversational Systems: Their Role in Referring Expressions. - Gopalan Nadathur; Aravind K. Joshi (IJCAI, 1983)

Some Uses of Higher-Order Logic in Computational Linguistics. - Dale Miller 001; Gopalan Nadathur (ACL, 1986)

Higher-Order Logic Programming. - Dale Miller 001; Gopalan Nadathur (ICLP, 1986)

Hereditary Harrop Formulas and Uniform Proof Systems - Dale Miller 001; Gopalan Nadathur; Andre Scedrov (LICS, 1987)

A Logic Programming Approach to Manipulating Formulas and Programs. - Dale Miller 001; Gopalan Nadathur (SLP, 1987)

Lambda-Prolog: An Extended Logic Programming Language. - Amy P. Felty; Elsa L. Gunter; John Hannan; Dale Miller 001; Gopalan Nadathur; Andre Scedrov (CADE, 1988)

An Overview of Lambda-PROLOG. - Gopalan Nadathur; Dale Miller 001 (ICLP/SLP, 1988)

Towards a WAM Model for Lambda-Prolog. - Gopalan Nadathur; Bharat Jayaraman (NACLP, 1989)

A Representation of Lambda Terms Suitable for Operations on Their Intensions. - Gopalan Nadathur; Debra Sue Wilson (LISP and Functional Programming, 1990)

Higher-Order Horn Clauses - Gopalan Nadathur; Dale Miller 001 (J. ACM, 1990)

Implementation Techniques for Scoping Constructs in Logic Programming. - Bharat Jayaraman; Gopalan Nadathur (ICLP, 1991)

Uniform Proofs as a Foundation for Logic Programming. - Dale Miller 001; Gopalan Nadathur; Frank Pfenning; Andre Scedrov (Ann. Pure Appl. Log., 1991)

The Type System of a Higher-Order Logic Programming Language. - Gopalan Nadathur; Frank Pfenning (Types in Logic Programming, 1992)

Implementing a Notion of Modules in the Logic Programming Language Lambda-Prolog. - Keehang Kwon; Gopalan Nadathur; Debra Sue Wilson (ELP, 1992)

A Proof Procedure for the Logic of Hereditary Harrop Formulas. - Gopalan Nadathur (J. Autom. Reason., 1993)

Implementing Polymorphic Typing in a Logic Programming Language. - Keehang Kwon; Gopalan Nadathur; Debra Sue Wilson (Comput. Lang., 1994)

Uniform Proofs and Disjunctive Logic Programming (Extended Abstract) - Gopalan Nadathur; Donald W. Loveland (LICS, 1995)

Scoping Constructs in Logic Programming: Implementation Problems and their Solutions. - Gopalan Nadathur; Bharat Jayaraman; Keehang Kwon (J. Log. Program., 1995)

Scoping Constructs in Logic Programming: Implementation Problems and their Solution - Gopalan Nadathur; Bharat Jayaraman; Keehang Kwon (CoRR, 1998)

Uniform Provability in Classical Logic. - Gopalan Nadathur (J. Log. Comput., 1998)

A Notation for Lambda Terms: A Generalization of Environments. - Gopalan Nadathur; Debra Sue Wilson (Theor. Comput. Sci., 1998)

System Description: Teyjus - A Compiler and Abstract Machine Based Implementation of lambda-Prolog. - Gopalan Nadathur; Dustin J. Mitchell (CADE, 1999)

A Fine-Grained Notation for Lambda Terms and Its Use in Intensional Operations. - Gopalan Nadathur (J. Funct. Log. Program., 1999)

Realizing Modularity in lambdaProlog. - Gopalan Nadathur; Guanshan Tong (J. Funct. Log. Program., 1999)

A framework for realizing derivation systems. - Gopalan Nadathur (ACM SIGSOFT Softw. Eng. Notes, 2000)

Correspondences between classical, intuitionistic and uniform provability. - Gopalan Nadathur (Theor. Comput. Sci., 2000)

The Metalanguage lambda-Prolog and Its Implementation. - Gopalan Nadathur (FLOPS, 2001)

Tradeoffs in the Intensional Representation of Lambda Terms. - Chuck C. Liang; Gopalan Nadathur (RTA, 2002)

The Suspension Notation for Lambda Terms and its Use in Metalanguage Implementations. - Gopalan Nadathur (WoLLIC, 2002)

Explicit substitutions in the reduction of lambda terms. - Gopalan Nadathur; Xiaochu Qi (PPDP, 2003)

Choices in Representation and Reduction Strategies for Lambda Terms in Intensional Contexts. - Chuck C. Liang; Gopalan Nadathur; Xiaochu Qi (J. Autom. Reason., 2004)

Testing Concurrent Systems: An Interpretation of Intuitionistic Logic. - Radha Jagadeesan; Gopalan Nadathur; Vijay A. Saraswat (FSTTCS, 2005)

Practical Higher-Order Pattern Unification with On-the-Fly Raising. - Gopalan Nadathur; Natalie Linnell (ICLP, 2005)

Optimizing the Runtime Processing of Types in Polymorphic Logic Programming Languages. - Gopalan Nadathur; Xiaochu Qi (LPAR, 2005)

A treatment of higher-order features in logic programming. - Gopalan Nadathur (Theory Pract. Log. Program., 2005)

The Bedwyr System for Model Checking over Syntactic Expressions. - David Baelde; Andrew Gacek; Dale Miller 001; Gopalan Nadathur; Alwen Tiu (CADE, 2007)

A Simplified Suspension Calculus and its Relationship to Other Explicit Substitution Calculi - Andrew Gacek; Gopalan Nadathur (CoRR, 2007)

Combining Generic Judgments with Recursive Definitions. - Andrew Gacek; Dale Miller 001; Gopalan Nadathur (LICS, 2008)

Reasoning in Abella about Structural Operational Semantics Specifications. - Andrew Gacek; Dale Miller 001; Gopalan Nadathur (LFMTP@LICS, 2008)

A meta-programming approach to realizing dependently typed logic programming. - Zachary Snow; David Baelde; Gopalan Nadathur (PPDP, 2010)

Redundancies in Dependently Typed Lambda Calculi and Their Relevance to Proof Search - Zachary Snow; David Baelde; Gopalan Nadathur (CoRR, 2010)

Nominal abstraction. - Andrew Gacek; Dale Miller 001; Gopalan Nadathur (Inf. Comput., 2011)

Programming with Higher-Order Logic. - Dale Miller 001; Gopalan Nadathur (Cambridge University Press, 2012)

Combining Deduction Modulo and Logics of Fixed-Point Definitions. - David Baelde; Gopalan Nadathur (LICS, 2012)

A Two-Level Logic Approach to Reasoning About Computations. - Andrew Gacek; Dale Miller 001; Gopalan Nadathur (J. Autom. Reason., 2012)

Towards extracting explicit proofs from totality checking in twelf. - Yuting Wang 001; Gopalan Nadathur (LFMTP, 2013)

Reasoning about higher-order relational specifications. - Yuting Wang 001; Kaustuv Chaudhuri; Andrew Gacek; Gopalan Nadathur (PPDP, 2013)

Translating Specifications in a Dependently Typed Lambda Calculus into a Predicate Logic Form. - Mary Southern; Gopalan Nadathur (CoRR, 2013)

A Framework for the Verified Transformation of Functional Programs. - Gopalan Nadathur (LFMTP, 2014)

A Lambda Prolog Based Animation of Twelf Specifications. - Mary Southern; Gopalan Nadathur (CoRR, 2014)

Abella: A System for Reasoning about Relational Specifications. - David Baelde; Kaustuv Chaudhuri; Andrew Gacek; Dale Miller 001; Gopalan Nadathur; Alwen Tiu; Yuting Wang 001 (J. Formaliz. Reason., 2014)

Verified Transformations on Functional Programs Using the Higher-Order Abstract Syntax Approach. - Yuting Wang 001; Gopalan Nadathur (CoRR, 2015)

A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs. - Yuting Wang 001; Gopalan Nadathur (ESOP, 2016)

Schematic Polymorphism in the Abella Proof Assistant. - Gopalan Nadathur; Yuting Wang 001 (PPDP, 2018)

Towards a Logic for Reasoning About LF Specifications. - Mary Southern; Gopalan Nadathur (CoRR, 2018)

A special issue on structural proof theory, automated reasoning and computation in celebration of Dale Miller's 60th birthday. - David Baelde; Amy P. Felty; Gopalan Nadathur; Alexis Saurin (Math. Struct. Comput. Sci., 2019)

A Logic for Reasoning About LF Specifications. - Gopalan Nadathur; Mary Southern (CoRR, 2021)

Adelfa: A System for Reasoning about LF Specifications. - Mary Southern; Gopalan Nadathur (LFMTP, 2021)

On Encoding LF in a Predicate Logic over Simply-Typed Lambda Terms. - Gopalan Nadathur; Mary Southern (CoRR, 2021)

About a Proof Pearl: A Purported Solution to a POPLMARK Challenge Problem that is Not One. - Gopalan Nadathur (CoRR, 2021)

A Logic for Formalizing Properties of LF Specifications. - Gopalan Nadathur; Mary Southern (PPDP, 2022)

Modularity and Separate Compilation in Logic Programming. - Steven Holte; Gopalan Nadathur (CoRR, 2023)

A Modular Approach to Metatheoretic Reasoning for Extensible Languages. - Dawn Michaelson; Gopalan Nadathur; Eric Van Wyk (CoRR, 2023)

Binding Contexts as Partitionable Multisets in Abella. - Terrance Gray; Gopalan Nadathur (LFMTP@FSCD, 2024)