Gopalan Nadathur

83 papers A* 6A 4B 4C 8Misc 1Journal 44Unranked 13

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