Gopalan Nadathur's Papers (Partial List)

Listed below in reverse-chronological order are several of my papers starting from 1993 onwards. I intend to sort these according to topic at some point. In the meantime, I hope you know what you are looking for and are able to find it here. If not, send me mail and I will try to help you figure out what it is that you need and/or to locate it.


Teyjus: A λProlog Implementation, Gopalan Nadathur. An article written for the Association of Logic Programming Newsletter, May 2009.
(
PDF)

An Approach to Modularity and Separate Compilation in Logic Programming, Steven Holte and Gopalan Nadathur. (Draft of May 2009.)
(
Abstract)(PDF)

Reasoning in Abella About Structural Operational Semantics Specifications, Andrew Gacek, Dale Miller and Gopalan Nadathur. Appears in the Proceedings of the Logical Frameworks and Metalanguages--Theory and Practice (LFMTP) Workshop, Electronic Notes in Theoretical Computer Science (2009): 85--100, Elsevier, 2009.
(
Abstract)(PDF)

Combining Generic Judgments with Recursive Definitions, Andrew Gacek, Dale Miller and Gopalan Nadathur. Appears in Proceedings of the Twenty-third Annual IEEE Symposium on Logic in Computer Science, pages 33--44, IEEE Computer Society Press, June 2008.
(
Abstract)(PDF)

A Simplified Suspension Calculus and its Relationship to Other Explicit Substitution Calculi, Andrew Gacek and Gopalan Nadathur. Research Report 2007/39, Digital Technology Center, University of Minnesota.
(
Abstract)(PDF)

The Bedwyr System for Model Checking over Syntactic Expressions, David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur and Alwen Tiu. Appears in 21st Conference on Automated Deduction, Springer LNAI 4603, pages 391-397, 2007.
(
Abstract)(PDF)

Testing Concurrent Systems: An Interpretation of Intuitionistic Logic, Radha Jagadeesan, Gopalan Nadathur and Vijay Saraswat. Revised version appears in 25th Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Springer LNCS 3821, pages 517-528, 2005.
(
Abstract) (PDF)

Optimizing the Runtime Processing of Types in a Higher-Order Logic Programming Language, Gopalan Nadathur and Xiaochu Qi. Revised version appears in Twelfth International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'05), Springer LNAI 3835, pages 110-125, 2005.
(
Abstract) (PS) (PDF)

Mixing Finite Success and Finite Failure in a Theorem Prover, Alwen Tiu, Gopalan Nadathur and Dale Miller. Appears in Workshop on Empirically Successful Automated Reasoning in Higher-Order Logic (ESHOL'05), 2005.
(
Abstract)(PDF)

An SML Implementation of Higher-Order Pattern Unification, Gopalan Nadathur and Natalie Linnell.
(
tar file version of Jan 23, 2006)

Practical Higher-Order Pattern Unification With On-the-Fly Raising, Gopalan Nadathur and Natalie Linnell. Revised version appears Twenty-First International Conference on Logic Programming, Lecture Notes in Computer Science Vol 3668, pages 371-387, Springer, 2005.
(
Abstract)(PS) (PDF)

Choices in representation and reduction strategies for lambda terms in intensional contexts, Chuck Liang, Gopalan Nadathur and Xiaochu Qi. Revised version appears in Journal of Automated Reasoning 33: 89-132, 2005.
(
Abstract)(PS)(PDF)

Explicit Substitutions in the Reduction of Lambda Terms, Gopalan Nadathur and Xiaochu Qi. Appears in Fifth ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming, pages 195-206, 2003. (Abstract)(PS)(PDF)

A Treatment of Higher-Order Features in Logic Programming, Gopalan Nadathur. Revised version appears in Theory and Practice of Logic Programming 5(3): 305 -- 354, 2005.
(
Abstract)(PS)(PDF)

The Suspension Notation for Lambda Terms and its Use in Metalanguage Implementations, Gopalan Nadathur. Ninth Workshop on Logic, Language, Information and Computation (WoLLIC'02), Electronic Notes in Theoretical Computer Science, Volume 67, Elsevier, 2002.
(Abstract)(PS)(PDF)(Journal Page)

Tradeoffs in the Intensional Representation of Lambda Terms, Chuck Liang and Gopalan Nadathur. Appears in Proceedings of the Thirteenth International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science, Volume 2378, (S. Tison, ed.), pages 192-206, Springer-Verlag, 2002.
(
Abstract)(PS)(PDF)

The Metalanguage Lambda Prolog and Its Implementation, Gopalan Nadathur. Appears in Proceedings of the Fifth International Symposium on Functional and Logic Programming, Lecture Notes in Computer Science, Volume 2024, (H. Kuchen and K. Ueda, eds.), pages 1--20, Springer-Verlag, 2001.
(
Abstract)(PS)(PDF)

System Description: Teyjus-A Compiler and Abstract Machine Based Implementation of Lambda Prolog, Gopalan Nadathur and Dustin J. Mitchell. Appears in Sixteenth Conference on Automated Deduction, H. Ganzinger (ed.), pages 287-291, 1999.
(
Abstract)(PS)(PDF)

An Explicit Substitution Notation in a lambdaProlog Implementation Gopalan Nadathur. Appears in Proceedings of the First International Workshop on Explicit Substitutions, Tsukuba, Japan. Also available as Technical Report Number TR-98-01, Department of Computer Science, University of Chicago, January, 1998.
(
Abstract)(PS)(PDF)

Correspondences between Classical, Intuitionistic and Uniform Provability Gopalan Nadathur. Revised version appears in Theoretical Computer Science 232(1-2):273--298, 2000. Also available as Technical Report Number TR-97-12, CS Department, University of Chicago.
(
Abstract)(PS)

Realizing Modularity in lambdaProlog. Gopalan Nadathur and Guanshan Tong. Appears in Journal of Functional and Logic Programming 1999(9), MIT Press, April 1999.
(
Abstract)(PDF)(Journal Page)

A Fine-Grained Notation for Lambda Terms and Its Use in Intensional Operations. Appears in Journal of Functional and Logic Programming 1999(2), MIT Press, March 1999. (Previously available as Duke Technical Report CS-1994-01.)
(
Abstract) (Journal page)

A Notation for Lambda Terms: A Generalization of Environments. Gopalan Nadathur and Debra Sue Wilson. Revised version appears in Theoretical Computer Science 198(1-2):49-98, May 1998. Previously available as Technical Report TR-97-01, Department of Computer Science, University of Chicago.
(
Abstract) (DVI) (PS)

Higher-Order Logic Programming. Gopalan Nadathur and Dale Miller. Appears in Handbook of Logic in AI and Logic Programming, Volume 5, Oxford University Press, pp 499-590, 1998.
(
Abstract) (DVI) (PS)

Proof Procedures in Logic Programming. Donald Loveland and Gopalan Nadathur. Appears in Handbook of Logic in AI and Logic Programming, Volume 5, Oxford University Press, pp 163-234, 1998.
(
Abstract) (DVI) (PS)

Uniform Provability in Classical Logic. Gopalan Nadathur. Technical Report Number TR-96-09, CS Department, University of Chicago. Appears in Journal of Logic and Computation 8(2):209-230, 1998.
(
Abstract) (PS)

Uniform Proofs and Disjunctive Logic Programming. Gopalan Nadathur and Donald Loveland. Appears in the Tenth Annual Symposium on Logic in Computer Science, pages 148-155, July 1995.
(Abstract) (PDF) (PS) (DVI)

Scoping Constructs in Logic Programming: Implementation Problems and their Solution. Gopalan Nadathur, Bharat Jayaraman and Keehang Kwon. Appears in Journal of Logic Programming 25(2): 119-161, November 1995.
(
Abstract) (DVI) (PS) (PDF)

Implementing Polymorphic Typing in a Logic Programming Language. Keehang Kwon, Gopalan Nadathur and Debra Sue Wilson. Appears in Computer Languages 20(1): 25-42, 1994.
(
Abstract)(DVI)(PS)(PDF)

A Proof Procedure for the Logic of Hereditary Harrop Formulas. Gopalan Nadathur. Appears in Journal of Automated Reasoning 11: 115-145, 1993.
(
Abstract) (DVI) (PS)

Implementing a Notion of Modules in the Logic Programming Language λProlog. Keehang Kwon, Gopalan Nadathur and Debra Sue Wilson. Duke Technical Report CS-1993-18. Also appears in Proceedings of the Third International Workshop on Extensions of Logic Programming, Lecture Notes in Artificial Intelligence, Volume 660, pages 359--393, Springer Verlag, 1993.
(
Abstract) (DVI)(PS)


Last updated on May 19, 2009 by gopalan atsign cs.umn.edu