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