default search action
Gopalan Nadathur
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [c33]Terrance Gray, Gopalan Nadathur:
Binding Contexts as Partitionable Multisets in Abella. LFMTP@FSCD 2024: 19-34 - 2023
- [i25]Steven Holte, Gopalan Nadathur:
Modularity and Separate Compilation in Logic Programming. CoRR abs/2303.10453 (2023) - [i24]Dawn Michaelson, Gopalan Nadathur, Eric Van Wyk:
A Modular Approach to Metatheoretic Reasoning for Extensible Languages. CoRR abs/2312.14374 (2023) - 2022
- [c32]Gopalan Nadathur, Mary Southern:
A Logic for Formalizing Properties of LF Specifications. PPDP 2022: 6:1-6:13 - 2021
- [c31]Mary Southern, Gopalan Nadathur:
Adelfa: A System for Reasoning about LF Specifications. LFMTP 2021: 104-120 - [i23]Gopalan Nadathur, Mary Southern:
A Logic for Reasoning About LF Specifications. CoRR abs/2107.00111 (2021) - [i22]Gopalan Nadathur, Mary Southern:
On Encoding LF in a Predicate Logic over Simply-Typed Lambda Terms. CoRR abs/2108.10848 (2021) - [i21]Gopalan Nadathur:
About a Proof Pearl: A Purported Solution to a POPLMARK Challenge Problem that is Not One. CoRR abs/2112.09274 (2021)
2010 – 2019
- 2019
- [j17]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): 1007-1008 (2019) - 2018
- [c30]Gopalan Nadathur, Yuting Wang
Schematic Polymorphism in the Abella Proof Assistant. PPDP 2018: 15:1-15:13 - [i20]Gopalan Nadathur, Yuting Wang:
Schematic Polymorphism in the Abella Proof Assistant. CoRR abs/1806.07523 (2018) - [i19]Mary Southern, Gopalan Nadathur:
Towards a Logic for Reasoning About LF Specifications. CoRR abs/1806.10199 (2018) - 2016
- [c29]Yuting Wang
A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs. ESOP 2016: 752-779 - 2015
- [i18]Yuting Wang, Gopalan Nadathur:
Verified Transformations on Functional Programs Using the Higher-Order Abstract Syntax Approach. CoRR abs/1509.03705 (2015) - 2014
- [j16]David Baelde
Abella: A System for Reasoning about Relational Specifications. J. Formaliz. Reason. 7(2): 1-89 (2014) - [c28]Gopalan Nadathur:
A Framework for the Verified Transformation of Functional Programs. LFMTP 2014: 3: 1 - [i17]Mary Southern, Gopalan Nadathur:
A Lambda Prolog Based Animation of Twelf Specifications. CoRR abs/1407.1545 (2014) - 2013
- [c27]Yuting Wang
Towards extracting explicit proofs from totality checking in twelf. LFMTP 2013: 55-66 - [c26]Yuting Wang
Reasoning about higher-order relational specifications. PPDP 2013: 157-168 - [i16]Yuting Wang, Kaustuv Chaudhuri, Andrew Gacek, Gopalan Nadathur:
Reasoning About Higher-Order Relational Specifications. CoRR abs/1302.2584 (2013) - [i15]Yuting Wang, Gopalan Nadathur:
Towards Extracting Explicit Proofs from Totality Checking in Twelf. CoRR abs/1307.1738 (2013) - [i14]Mary Southern, Gopalan Nadathur:
Translating Specifications in a Dependently Typed Lambda Calculus into a Predicate Logic Form. CoRR abs/1310.8568 (2013) - 2012
- [b1]Dale Miller, Gopalan Nadathur:
Programming with Higher-Order Logic. Cambridge University Press 2012, ISBN 978-0-521-87940-8, pp. I-XIII, 1-306 - [j15]Andrew Gacek, Dale Miller
A Two-Level Logic Approach to Reasoning About Computations. J. Autom. Reason. 49(2): 241-273 (2012) - [c25]David Baelde, Gopalan Nadathur:
Combining Deduction Modulo and Logics of Fixed-Point Definitions. LICS 2012: 105-114 - [i13]David Baelde, Gopalan Nadathur:
Combining Deduction Modulo and Logics of Fixed-Point Definitions. CoRR abs/1204.6236 (2012) - 2011
- [j14]Andrew Gacek, Dale Miller
Nominal abstraction. Inf. Comput. 209(1): 48-73 (2011) - [e2]Herman Geuvers, Gopalan Nadathur:
Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP 2011, Nijmegen, The Netherlands, August 26, 2011. EPTCS 71, 2011 [contents] - 2010
- [c24]Zachary Snow, David Baelde, Gopalan Nadathur:
A meta-programming approach to realizing dependently typed logic programming. PPDP 2010: 187-198 - [i12]Zachary Snow, David Baelde, Gopalan Nadathur:
A Meta-Programming Approach to Realizing Dependently Typed Logic Programming. CoRR abs/1005.4379 (2010) - [i11]Zachary Snow, David Baelde, Gopalan Nadathur:
Redundancies in Dependently Typed Lambda Calculi and Their Relevance to Proof Search. CoRR abs/1007.0779 (2010)
2000 – 2009
- 2009
- [i10]Andrew Gacek, Dale Miller, Gopalan Nadathur:
Nominal Abstraction. CoRR abs/0908.1390 (2009) - [i9]Andrew Gacek, Dale Miller, Gopalan Nadathur:
A two-level logic approach to reasoning about computations. CoRR abs/0911.2993 (2009) - 2008
- [c23]Andrew Gacek, Dale Miller
Combining Generic Judgments with Recursive Definitions. LICS 2008: 33-44 - [c22]Andrew Gacek, Dale Miller
Reasoning in Abella about Structural Operational Semantics Specifications. LFMTP@LICS 2008: 85-100 - [i8]Andrew Gacek, Dale Miller, Gopalan Nadathur:
Combining generic judgments with recursive definitions. CoRR abs/0802.0865 (2008) - [i7]Andrew Gacek, Dale Miller, Gopalan Nadathur:
Reasoning in Abella about Structural Operational Semantics Specifications. CoRR abs/0804.3914 (2008) - 2007
- [c21]David Baelde, Andrew Gacek, Dale Miller
The Bedwyr System for Model Checking over Syntactic Expressions. CADE 2007: 391-397 - [i6]David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu:
The Bedwyr system for model checking over syntactic expressions. CoRR abs/cs/0702116 (2007) - [i5]Andrew Gacek, Gopalan Nadathur:
A Simplified Suspension Calculus and its Relationship to Other Explicit Substitution Calculi. CoRR abs/cs/0702152 (2007) - 2005
- [j13]Gopalan Nadathur:
A treatment of higher-order features in logic programming. Theory Pract. Log. Program. 5(3): 305-354 (2005) - [c20]Radha Jagadeesan, Gopalan Nadathur, Vijay A. Saraswat:
Testing Concurrent Systems: An Interpretation of Intuitionistic Logic. FSTTCS 2005: 517-528 - [c19]Gopalan Nadathur, Natalie Linnell:
Practical Higher-Order Pattern Unification with On-the-Fly Raising. ICLP 2005: 371-386 - [c18]Gopalan Nadathur, Xiaochu Qi:
Optimizing the Runtime Processing of Types in Polymorphic Logic Programming Languages. LPAR 2005: 110-124 - 2004
- [j12]Chuck C. Liang, Gopalan Nadathur, Xiaochu Qi:
Choices in Representation and Reduction Strategies for Lambda Terms in Intensional Contexts. J. Autom. Reason. 33(2): 89-132 (2004) - [i4]Gopalan Nadathur:
A treatment of higher-order features in logic programming. CoRR cs.PL/0404020 (2004) - 2003
- [c17]Gopalan Nadathur, Xiaochu Qi:
Explicit substitutions in the reduction of lambda terms. PPDP 2003: 195-206 - 2002
- [c16]Chuck C. Liang, Gopalan Nadathur:
Tradeoffs in the Intensional Representation of Lambda Terms. RTA 2002: 192-206 - [c15]Gopalan Nadathur:
The Suspension Notation for Lambda Terms and its Use in Metalanguage Implementations. WoLLIC 2002: 35-48 - 2001
- [c14]Gopalan Nadathur:
The Metalanguage lambda-Prolog and Its Implementation. FLOPS 2001: 1-20 - 2000
- [j11]Gopalan Nadathur:
A framework for realizing derivation systems. ACM SIGSOFT Softw. Eng. Notes 25(1): 66-67 (2000) - [j10]Gopalan Nadathur:
Correspondences between classical, intuitionistic and uniform provability. Theor. Comput. Sci. 232(1-2): 273-298 (2000)
1990 – 1999
- 1999
- [j9]Gopalan Nadathur:
A Fine-Grained Notation for Lambda Terms and Its Use in Intensional Operations. J. Funct. Log. Program. 1999(2) (1999) - [j8]Gopalan Nadathur, Guanshan Tong:
Realizing Modularity in lambdaProlog. J. Funct. Log. Program. 1999(Special Issue 1) (1999) - [c13]Gopalan Nadathur, Dustin J. Mitchell:
System Description: Teyjus - A Compiler and Abstract Machine Based Implementation of lambda-Prolog. CADE 1999: 287-291 - [e1]Gopalan Nadathur:
Principles and Practice of Declarative Programming, International Conference PPDP'99, Paris, France, September 29 - October 1, 1999, Proceedings. Lecture Notes in Computer Science 1702, Springer 1999, ISBN 3-540-66540-4 [contents] - 1998
- [j7]Gopalan Nadathur:
Uniform Provability in Classical Logic. J. Log. Comput. 8(2): 209-229 (1998) - [j6]Gopalan Nadathur, Debra Sue Wilson:
A Notation for Lambda Terms: A Generalization of Environments. Theor. Comput. Sci. 198(1-2): 49-98 (1998) - [i3]Gopalan Nadathur:
Uniform Provability in Classical Logic. CoRR cs.LO/9809014 (1998) - [i2]Gopalan Nadathur:
Correspondences between Classical, Intuitionistic and Uniform Provability. CoRR cs.LO/9809015 (1998) - [i1]Gopalan Nadathur, Bharat Jayaraman, Keehang Kwon:
Scoping Constructs in Logic Programming: Implementation Problems and their Solution. CoRR cs.PL/9809016 (1998) - 1995
- [j5]Gopalan Nadathur, Bharat Jayaraman, Keehang Kwon:
Scoping Constructs in Logic Programming: Implementation Problems and their Solutions. J. Log. Program. 25(2): 119-161 (1995) - [c12]Gopalan Nadathur, Donald W. Loveland:
Uniform Proofs and Disjunctive Logic Programming (Extended Abstract). LICS 1995: 148-155 - 1994
- [j4]Keehang Kwon, Gopalan Nadathur, Debra Sue Wilson:
Implementing Polymorphic Typing in a Logic Programming Language. Comput. Lang. 20(1): 25-42 (1994) - 1993
- [j3]Gopalan Nadathur:
A Proof Procedure for the Logic of Hereditary Harrop Formulas. J. Autom. Reason. 11(1): 115-145 (1993) - 1992
- [c11]Keehang Kwon, Gopalan Nadathur, Debra Sue Wilson:
Implementing a Notion of Modules in the Logic Programming Language Lambda-Prolog. ELP 1992: 359-393 - [p1]Gopalan Nadathur, Frank Pfenning:
The Type System of a Higher-Order Logic Programming Language. Types in Logic Programming 1992: 245-283 - 1991
- [j2]Dale Miller
Uniform Proofs as a Foundation for Logic Programming. Ann. Pure Appl. Log. 51(1-2): 125-157 (1991) - [c10]Bharat Jayaraman, Gopalan Nadathur:
Implementation Techniques for Scoping Constructs in Logic Programming. ICLP 1991: 871-886 - 1990
- [j1]Gopalan Nadathur, Dale Miller
Higher-Order Horn Clauses. J. ACM 37(4): 777-814 (1990) - [c9]Gopalan Nadathur, Debra Sue Wilson:
A Representation of Lambda Terms Suitable for Operations on Their Intensions. LISP and Functional Programming 1990: 341-348
1980 – 1989
- 1989
- [c8]Gopalan Nadathur, Bharat Jayaraman:
Towards a WAM Model for Lambda-Prolog. NACLP 1989: 1180-1198 - 1988
- [c7]Amy P. Felty, Elsa L. Gunter, John Hannan, Dale Miller
Lambda-Prolog: An Extended Logic Programming Language. CADE 1988: 754-755 - [c6]Gopalan Nadathur, Dale Miller:
An Overview of Lambda-PROLOG. ICLP/SLP 1988: 810-827 - 1987
- [c5]Dale Miller, Gopalan Nadathur, Andre Scedrov:
Hereditary Harrop Formulas and Uniform Proof Systems. LICS 1987: 98-105 - [c4]Dale Miller, Gopalan Nadathur:
A Logic Programming Approach to Manipulating Formulas and Programs. SLP 1987: 379-388 - 1986
- [c3]Dale Miller, Gopalan Nadathur:
Some Uses of Higher-Order Logic in Computational Linguistics. ACL 1986: 247-256 - [c2]Dale Miller
Higher-Order Logic Programming. ICLP 1986: 448-462 - 1983
- [c1]Gopalan Nadathur, Aravind K. Joshi:
Mutual Beliefs in Conversational Systems: Their Role in Referring Expressions. IJCAI 1983: 603-605
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-11-04 20:38 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: