Gopalan Nadathur

Publication Activity (10 Years)

Years Active: 1983-2024
Publications (10 Years): 14

Top Topics

Lazy Evaluation

Automated Reasoning

Delay Insensitive

Top Venues

J. Formaliz. Reason.

Publications

Terrance Gray, Gopalan Nadathur
Binding Contexts as Partitionable Multisets in Abella. CoRR (2024)
Dawn Michaelson, Gopalan Nadathur, Eric Van Wyk
A Modular Approach to Metatheoretic Reasoning for Extensible Languages. CoRR (2023)
Steven Holte, Gopalan Nadathur
Modularity and Separate Compilation in Logic Programming. CoRR (2023)
Gopalan Nadathur, Mary Southern
A Logic for Formalizing Properties of LF Specifications. PPDP (2022)
Gopalan Nadathur
About a Proof Pearl: A Purported Solution to a POPLMARK Challenge Problem that is Not One. CoRR (2021)
Gopalan Nadathur, Mary Southern
A Logic for Reasoning About LF Specifications. CoRR (2021)
Gopalan Nadathur, Mary Southern
On Encoding LF in a Predicate Logic over Simply-Typed Lambda Terms. CoRR (2021)
Mary Southern, Gopalan Nadathur
Adelfa: A System for Reasoning about LF Specifications. LFMTP (2021)
David Baelde, Amy P. Felty, Gopalan Nadathur, Alexis Saurin
A special issue on structural proof theory, automated reasoning and computation in celebration of Dale Miller's 60th birthday. Math. Struct. Comput. Sci. 29 (8) (2019)
Mary Southern, Gopalan Nadathur
Towards a Logic for Reasoning About LF Specifications. CoRR (2018)
Gopalan Nadathur, Yuting Wang
Schematic Polymorphism in the Abella Proof Assistant. PPDP (2018)
Gopalan Nadathur, Yuting Wang
Schematic Polymorphism in the Abella Proof Assistant. CoRR (2018)
Yuting Wang, Gopalan Nadathur
A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs. ESOP (2016)
Yuting Wang, Gopalan Nadathur
Verified Transformations on Functional Programs Using the Higher-Order Abstract Syntax Approach. CoRR (2015)
David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, Yuting Wang
Abella: A System for Reasoning about Relational Specifications. J. Formaliz. Reason. 7 (2) (2014)
Gopalan Nadathur
A Framework for the Verified Transformation of Functional Programs. LFMTP (2014)
Mary Southern, Gopalan Nadathur
A Lambda Prolog Based Animation of Twelf Specifications. CoRR (2014)
Yuting Wang, Gopalan Nadathur
Towards Extracting Explicit Proofs from Totality Checking in Twelf. CoRR (2013)
Yuting Wang, Kaustuv Chaudhuri, Andrew Gacek, Gopalan Nadathur
Reasoning About Higher-Order Relational Specifications CoRR (2013)
Yuting Wang, Kaustuv Chaudhuri, Andrew Gacek, Gopalan Nadathur
Reasoning about higher-order relational specifications. PPDP (2013)
Mary Southern, Gopalan Nadathur
Translating Specifications in a Dependently Typed Lambda Calculus into a Predicate Logic Form. CoRR (2013)
Yuting Wang, Gopalan Nadathur
Towards extracting explicit proofs from totality checking in twelf. LFMTP (2013)
Andrew Gacek, Dale Miller, Gopalan Nadathur
A Two-Level Logic Approach to Reasoning About Computations. J. Autom. Reason. 49 (2) (2012)
David Baelde, Gopalan Nadathur
Combining Deduction Modulo and Logics of Fixed-Point Definitions CoRR (2012)
David Baelde, Gopalan Nadathur
Combining Deduction Modulo and Logics of Fixed-Point Definitions. LICS (2012)
Andrew Gacek, Dale Miller, Gopalan Nadathur
Nominal abstraction. Inf. Comput. 209 (1) (2011)
Zachary Snow, David Baelde, Gopalan Nadathur
A Meta-Programming Approach to Realizing Dependently Typed Logic Programming CoRR (2010)
Zachary Snow, David Baelde, Gopalan Nadathur
A meta-programming approach to realizing dependently typed logic programming. PPDP (2010)
Zachary Snow, David Baelde, Gopalan Nadathur
Redundancies in Dependently Typed Lambda Calculi and Their Relevance to Proof Search CoRR (2010)
Andrew Gacek, Dale Miller, Gopalan Nadathur
A two-level logic approach to reasoning about computations CoRR (2009)
Andrew Gacek, Dale Miller, Gopalan Nadathur
Reasoning in Abella about Structural Operational Semantics Specifications. Electron. Notes Theor. Comput. Sci. 228 (2009)
Andrew Gacek, Dale Miller, Gopalan Nadathur
Nominal Abstraction CoRR (2009)
Andrew Gacek, Dale Miller, Gopalan Nadathur
Combining generic judgments with recursive definitions CoRR (2008)
Andrew Gacek, Dale Miller, Gopalan Nadathur
Reasoning in Abella about Structural Operational Semantics Specifications CoRR (2008)
Andrew Gacek, Dale Miller, Gopalan Nadathur
Combining Generic Judgments with Recursive Definitions. LICS (2008)
David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu
The Bedwyr system for model checking over syntactic expressions CoRR (2007)
Andrew Gacek, Gopalan Nadathur
A Simplified Suspension Calculus and its Relationship to Other Explicit Substitution Calculi CoRR (2007)
David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu
The Bedwyr System for Model Checking over Syntactic Expressions. CADE (2007)
Gopalan Nadathur, Natalie Linnell
Practical Higher-Order Pattern Unification with On-the-Fly Raising. ICLP (2005)
Gopalan Nadathur, Xiaochu Qi
Optimizing the Runtime Processing of Types in Polymorphic Logic Programming Languages. LPAR (2005)
Gopalan Nadathur
A treatment of higher-order features in logic programming. Theory Pract. Log. Program. 5 (3) (2005)
Radha Jagadeesan, Gopalan Nadathur, Vijay A. Saraswat
Testing Concurrent Systems: An Interpretation of Intuitionistic Logic. FSTTCS (2005)
Chuck C. Liang, Gopalan Nadathur, Xiaochu Qi
Choices in Representation and Reduction Strategies for Lambda Terms in Intensional Contexts. J. Autom. Reason. 33 (2) (2004)
Gopalan Nadathur
A treatment of higher-order features in logic programming CoRR (2004)
Gopalan Nadathur, Xiaochu Qi
Explicit substitutions in the reduction of lambda terms. PPDP (2003)
Chuck C. Liang, Gopalan Nadathur
Tradeoffs in the Intensional Representation of Lambda Terms. RTA (2002)
Gopalan Nadathur
The Suspension Notation for Lambda Terms and its Use in Metalanguage Implementations. Electron. Notes Theor. Comput. Sci. 67 (2002)
Gopalan Nadathur
The Metalanguage lambda-Prolog and Its Implementation. FLOPS (2001)
Gopalan Nadathur
A framework for realizing derivation systems. ACM SIGSOFT Softw. Eng. Notes 25 (1) (2000)
Gopalan Nadathur
Correspondences between classical, intuitionistic and uniform provability. Theor. Comput. Sci. 232 (1-2) (2000)
Gopalan Nadathur
A Fine-Grained Notation for Lambda Terms and Its Use in Intensional Operations. J. Funct. Log. Program. 1999 (2) (1999)
Gopalan Nadathur, Guanshan Tong
Realizing Modularity in lambdaProlog. J. Funct. Log. Program. 1999 (Special Issue 1) (1999)
Gopalan Nadathur, Dustin J. Mitchell
System Description: Teyjus - A Compiler and Abstract Machine Based Implementation of lambda-Prolog. CADE (1999)
Gopalan Nadathur
Correspondences between Classical, Intuitionistic and Uniform Provability CoRR (1998)
Gopalan Nadathur, Bharat Jayaraman, Keehang Kwon
Scoping Constructs in Logic Programming: Implementation Problems and their Solution CoRR (1998)
Gopalan Nadathur
Uniform Provability in Classical Logic. J. Log. Comput. 8 (2) (1998)
Gopalan Nadathur, Debra Sue Wilson
A Notation for Lambda Terms: A Generalization of Environments. Theor. Comput. Sci. 198 (1-2) (1998)
Gopalan Nadathur
Uniform Provability in Classical Logic CoRR (1998)
Gopalan Nadathur, Donald W. Loveland
Uniform Proofs and Disjunctive Logic Programming (Extended Abstract) LICS (1995)
Gopalan Nadathur, Bharat Jayaraman, Keehang Kwon
Scoping Constructs in Logic Programming: Implementation Problems and their Solutions. J. Log. Program. 25 (2) (1995)
Keehang Kwon, Gopalan Nadathur, Debra Sue Wilson
Implementing Polymorphic Typing in a Logic Programming Language. Comput. Lang. 20 (1) (1994)
Gopalan Nadathur
A Proof Procedure for the Logic of Hereditary Harrop Formulas. J. Autom. Reason. 11 (1) (1993)
Keehang Kwon, Gopalan Nadathur, Debra Sue Wilson
Implementing a Notion of Modules in the Logic Programming Language Lambda-Prolog. ELP (1992)
Dale Miller, Gopalan Nadathur, Frank Pfenning, Andre Scedrov
Uniform Proofs as a Foundation for Logic Programming. Ann. Pure Appl. Log. 51 (1-2) (1991)
Bharat Jayaraman, Gopalan Nadathur
Implementation Techniques for Scoping Constructs in Logic Programming. ICLP (1991)
Gopalan Nadathur, Dale Miller
Higher-Order Horn Clauses J. ACM 37 (4) (1990)
Gopalan Nadathur, Debra Sue Wilson
A Representation of Lambda Terms Suitable for Operations on Their Intensions. LISP and Functional Programming (1990)
Gopalan Nadathur, Bharat Jayaraman
Towards a WAM Model for Lambda-Prolog. NACLP (1989)
Gopalan Nadathur, Dale Miller
An Overview of Lambda-PROLOG. ICLP/SLP (1988)
Amy P. Felty, Elsa L. Gunter, John Hannan, Dale Miller, Gopalan Nadathur, Andre Scedrov
Lambda-Prolog: An Extended Logic Programming Language. CADE (1988)
Dale Miller, Gopalan Nadathur, Andre Scedrov
Hereditary Harrop Formulas and Uniform Proof Systems LICS (1987)
Dale Miller, Gopalan Nadathur
A Logic Programming Approach to Manipulating Formulas and Programs. SLP (1987)
Dale Miller, Gopalan Nadathur
Higher-Order Logic Programming. ICLP (1986)
Dale Miller, Gopalan Nadathur
Some Uses of Higher-Order Logic in Computational Linguistics. ACL (1986)
Gopalan Nadathur, Aravind K. Joshi
Mutual Beliefs in Conversational Systems: Their Role in Referring Expressions. IJCAI (1983)