Gopalan Nadathur

CoRR, 2021

On Encoding LF in a Predicate Logic over Simply-Typed Lambda Terms.

[BibT_eX]

[DOI]

CoRR, 2021

Adelfa: A System for Reasoning about LF Specifications.

[BibT_eX]

[DOI]

Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2021

A Logic for Reasoning About LF Specifications.

[BibT_eX]

[DOI]

CoRR, 2021

2019

A special issue on structural proof theory, automated reasoning and computation in celebration of Dale Miller's 60th birthday.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2019

2018

Towards a Logic for Reasoning About LF Specifications.

[BibT_eX]

[DOI]

CoRR, 2018

Schematic Polymorphism in the Abella Proof Assistant.

[BibT_eX]

[DOI]

Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, 2018

2016

A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2016

2015

Verified Transformations on Functional Programs Using the Higher-Order Abstract Syntax Approach.

[BibT_eX]

[DOI]

CoRR, 2015

2014

Abella: A System for Reasoning about Relational Specifications.

[BibT_eX]

[DOI]

J. Formaliz. Reason., 2014

A Lambda Prolog Based Animation of Twelf Specifications.

[BibT_eX]

[DOI]

CoRR, 2014

A Framework for the Verified Transformation of Functional Programs.

[BibT_eX]

[DOI]

Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, 2014

2013

Translating Specifications in a Dependently Typed Lambda Calculus into a Predicate Logic Form.

[BibT_eX]

[DOI]

CoRR, 2013

Reasoning about higher-order relational specifications.

[BibT_eX]

[DOI]

Proceedings of the 15th International Symposium on Principles and Practice of Declarative Programming, 2013

Towards extracting explicit proofs from totality checking in twelf.

[BibT_eX]

[DOI]

Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice, 2013

2012

A Two-Level Logic Approach to Reasoning About Computations.

[BibT_eX]

[DOI]

J. Autom. Reason., 2012

Combining Deduction Modulo and Logics of Fixed-Point Definitions.

[BibT_eX]

[DOI]

David Baelde

Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

Programming with Higher-Order Logic.

[BibT_eX]

[DOI]

Cambridge University Press, ISBN: 978-0-521-87940-8, 2012

2011

Nominal abstraction.

[BibT_eX]

[DOI]

Inf. Comput., 2011

2010

Redundancies in Dependently Typed Lambda Calculi and Their Relevance to Proof Search

[BibT_eX]

[DOI]

Zachary Snow

David Baelde

CoRR, 2010

A meta-programming approach to realizing dependently typed logic programming.

[BibT_eX]

[DOI]

Zachary Snow

David Baelde

Proceedings of the 12th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2010

2008

Reasoning in Abella about Structural Operational Semantics Specifications.

[BibT_eX]

[DOI]

Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, 2008

Combining Generic Judgments with Recursive Definitions.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, 2008

2007

A Simplified Suspension Calculus and its Relationship to Other Explicit Substitution Calculi

[BibT_eX]

[DOI]

CoRR, 2007

The Bedwyr System for Model Checking over Syntactic Expressions.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2007

2005

A treatment of higher-order features in logic programming.

[BibT_eX]

[DOI]

Theory Pract. Log. Program., 2005

Optimizing the Runtime Processing of Types in Polymorphic Logic Programming Languages.

[BibT_eX]

[DOI]

Xiaochu Qi

Proceedings of the Logic for Programming, 2005

Practical Higher-Order Pattern Unification with On-the-Fly Raising.

[BibT_eX]

[DOI]

Natalie Linnell

Proceedings of the Logic Programming, 21st International Conference, 2005

Testing Concurrent Systems: An Interpretation of Intuitionistic Logic.

[BibT_eX]

[DOI]

Radha Jagadeesan

Vijay A. Saraswat

Proceedings of the FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 2005

2004

Choices in Representation and Reduction Strategies for Lambda Terms in Intensional Contexts.

[BibT_eX]

[DOI]

Chuck C. Liang

Xiaochu Qi

J. Autom. Reason., 2004

2003

Explicit substitutions in the reduction of lambda terms.

[BibT_eX]

[DOI]

Xiaochu Qi

Proceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2003

2002

The Suspension Notation for Lambda Terms and its Use in Metalanguage Implementations.

[BibT_eX]

[DOI]

Proceedings of the 9th Workhop on Logic, Language, Information and Computation, 2002

Tradeoffs in the Intensional Representation of Lambda Terms.

[BibT_eX]

[DOI]

Chuck C. Liang

Proceedings of the Rewriting Techniques and Applications, 13th International Conference, 2002

2001

The Metalanguage lambda-Prolog and Its Implementation.

[BibT_eX]

[DOI]

Proceedings of the Functional and Logic Programming, 5th International Symposium, 2001

2000

Correspondences between classical, intuitionistic and uniform provability.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2000

A framework for realizing derivation systems.

[BibT_eX]

[DOI]

ACM SIGSOFT Softw. Eng. Notes, 2000

1999

Realizing Modularity in lambdaProlog.

[BibT_eX]

Guanshan Tong

J. Funct. Log. Program., 1999

A Fine-Grained Notation for Lambda Terms and Its Use in Intensional Operations.

[BibT_eX]

[DOI]

J. Funct. Log. Program., 1999

System Description: Teyjus - A Compiler and Abstract Machine Based Implementation of lambda-Prolog.

[BibT_eX]

[DOI]

Dustin J. Mitchell

Proceedings of the Automated Deduction, 1999

1998

A Notation for Lambda Terms: A Generalization of Environments.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1998

Uniform Provability in Classical Logic.

[BibT_eX]

[DOI]

J. Log. Comput., 1998

Scoping Constructs in Logic Programming: Implementation Problems and their Solution

[BibT_eX]

[DOI]

CoRR, 1998

1995

Scoping Constructs in Logic Programming: Implementation Problems and their Solutions.

[BibT_eX]

[DOI]

J. Log. Program., 1995

Uniform Proofs and Disjunctive Logic Programming (Extended Abstract)

[BibT_eX]

[DOI]

Donald W. Loveland

Proceedings of the Proceedings, 1995

1994

Implementing Polymorphic Typing in a Logic Programming Language.

[BibT_eX]

[DOI]

Comput. Lang., 1994

1993

A Proof Procedure for the Logic of Hereditary Harrop Formulas.

[BibT_eX]

[DOI]

J. Autom. Reason., 1993

1992

Implementing a Notion of Modules in the Logic Programming Language Lambda-Prolog.

[BibT_eX]

[DOI]

Proceedings of the Extensions of Logic Programming, Third International Workshop, 1992

The Type System of a Higher-Order Logic Programming Language.

[BibT_eX]

Frank Pfenning

Proceedings of the Types in Logic Programming., 1992

1991

Uniform Proofs as a Foundation for Logic Programming.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 1991

Implementation Techniques for Scoping Constructs in Logic Programming.

[BibT_eX]

Proceedings of the Logic Programming, 1991

1990

Higher-Order Horn Clauses

[BibT_eX]

[DOI]

J. ACM, October, 1990

A Representation of Lambda Terms Suitable for Operations on Their Intensions.

[BibT_eX]

[DOI]

Proceedings of the 1990 ACM Conference on LISP and Functional Programming, 1990

1989

Towards a WAM Model for Lambda-Prolog.

[BibT_eX]

Proceedings of the Logic Programming, 1989

1988

An Overview of Lambda-PROLOG.

[BibT_eX]

Proceedings of the Logic Programming, 1988

Lambda-Prolog: An Extended Logic Programming Language.

[BibT_eX]

[DOI]

Proceedings of the 9th International Conference on Automated Deduction, 1988

1987

A Logic Programming Approach to Manipulating Formulas and Programs.

[BibT_eX]

Proceedings of the 1987 Symposium on Logic Programming, San Francisco, California, USA, August 31, 1987

Hereditary Harrop Formulas and Uniform Proof Systems

[BibT_eX]

Andre Scedrov

Proceedings of the Symposium on Logic in Computer Science (LICS '87), 1987

1986

Higher-Order Logic Programming.

[BibT_eX]

[DOI]

Proceedings of the Third International Conference on Logic Programming, 1986

Some Uses of Higher-Order Logic in Computational Linguistics.

[BibT_eX]

[DOI]

Proceedings of the 24th Annual Meeting of the Association for Computational Linguistics, 1986

1983

Mutual Beliefs in Conversational Systems: Their Role in Referring Expressions.

[BibT_eX]

[DOI]