A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification

A formulation of the simple theory of types

Church, A. (1940) · Journal of Symbolic Logic · doi:10.2307/2266170 · Cited by 1,905 · see citing works

Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem

de Bruijn, N. G. (1972) · Indagationes Mathematicae (Proceedings) · doi:10.1016/1385-7258(72)90034-0 · Cited by 1,049 · see citing works

Investigations into Logical Deduction

Gentzen, G. (1964) · American Philosophical Quarterly · Cited by 659 · see citing works

Higher-order abstract syntax

Pfenning, F., & Elliott, C. M. (1988) · ACM SIGPLAN Notices · doi:10.1145/960116.54010 · Cited by 585 · see citing works

Uniform proofs as a foundation for logic programming

Miller, D., Nadathur, G., Pfenning, F., & Scedrov, A. (1991) · Annals of Pure and Applied Logic · doi:10.1016/0168-0072(91)90068-w · Cited by 570 · see citing works

The foundation of a generic theorem prover

Paulson, L. C. (1989) · Journal of Automated Reasoning · doi:10.1007/bf00248324 · Cited by 383 · see citing works

The undecidability of the second-order unification problem

Goldfarb, W. (1981) · Theoretical Computer Science · doi:10.1016/0304-3975(81)90040-2 · Cited by 280 · see citing works

A logical analysis of modules in logic programming

Miller, D. (1989) · The Journal of Logic Programming · doi:10.1016/0743-1066(89)90031-9 · Cited by 233 · see citing works

Intuitionistic propositional logic is polynomial-space complete

Statman, R. (1979) · Theoretical Computer Science · doi:10.1016/0304-3975(79)90006-9 · Cited by 231 · see citing works

Higher-order critical pairs

Nipkow, T. (2002) · ACM/IEEE Symposium on Logic in Computer Science (LICS) · doi:10.1109/lics.1991.151658 · Cited by 215 · see citing works

A framework for defining logics

Harper, R. W., Honsell, F., & Plotkin, G. D. (1993) · Journal of the ACM · doi:10.1145/138027.138060 · Cited by 192 · see citing works

Natural deduction as higher-order resolution

Paulson, L. C. (1986) · The Journal of Logic Programming · doi:10.1016/0743-1066(86)90015-4 · Cited by 154 · see citing works

Elf: a language for logic definition and verified metaprogramming

Pfenning, F. (2003) · doi:10.1109/lics.1989.39186 · Cited by 115 · see citing works

Unification and anti-unification in the calculus of constructions

Pfenning, F. (2002) · ACM/IEEE Symposium on Logic in Computer Science (LICS) · doi:10.1109/lics.1991.151632 · Cited by 115 · see citing works

Higher-order unification revisited: Complete sets of transformations

Snyder, W., & Gallier, J. H. (1989) · Journal of Symbolic Computation · doi:10.1016/s0747-7171(89)80023-9 · Cited by 113 · see citing works

A Logic Programming Approach To Manipulating Formulas And Programs

Miller, D., & Nadathur, G. (1987) · Cited by 108 · see citing works

Specifying theorem provers in a higher-order logic programming language

Felty, A., & Miller, D. (2005) · Springer eBooks · doi:10.1007/bfb0012823 · Cited by 105 · see citing works

Higher-order Horn clauses

Nadathur, G., & Miller, D. (1990) · Journal of the ACM · doi:10.1145/96559.96570 · Cited by 73 · see citing works

Unification of Simply Typed Lambda-Terms as Logic Programming

Miller, D. (1991) · ScholarlyCommons (University of Pennsylvania) · Cited by 69 · see citing works

Lexical Scoping as Universal Quantification

Miller, D. (1989) · ScholarlyCommons (University of Pennsylvania) · Cited by 64 · see citing works

Mechanizing ω-order type theory through unification

Jensen, D. C., & Pietrzykowski, T. (1976) · Theoretical Computer Science · doi:10.1016/0304-3975(76)90021-9 · Cited by 59 · see citing works

Uses of Higher-Order Unification for Implementing Program Transformers.

Hannan, J., & Miller, D. (1988) · Cited by 42 · see citing works

Abstractions in Logic Programs

Miller, D. (1989) · ScholarlyCommons (University of Pennsylvania) · Cited by 42 · see citing works

A representation of Lambda terms suitable for operations on their intensions

Nadathur, G., & Wilson, D. S. (1990) · ACM Conference on LISP and Functional Programming (LFP) · doi:10.1145/91556.91682 · Cited by 24 · see citing works

Constraint logic programming: a survey

Jaffar, J., & Maher, M. J. (1994) · The Journal of Logic Programming · doi:10.1016/0743-1066(94)90033-7 · Cited by 1,316 · see citing works

Contextual modal type theory

Nanevski, A., Pfenning, F., & Pientka, B. (2008) · ACM Transactions on Computational Logic · doi:10.1145/1352582.1352591 · Cited by 257 · see citing works

Rewriting Logic as a Logical and Semantic Framework

Martı́-Oliet, N., & Meseguer, J. (2002) · Springer eBooks · doi:10.1007/978-94-017-0464-9_1 · Cited by 252 · see citing works

Logical frameworks

Pfenning, F. (2001) · Cited by 218 · see citing works

Logic programming in the LF logical framework

Pfenning, F. (1991) · Cambridge University Press eBooks · doi:10.1017/cbo9780511569807.008 · Cited by 210 · see citing works

Nominal unification

Urban, C., Pitts, A. M., & Gabbay, M. J. (2004) · Theoretical Computer Science · doi:10.1016/j.tcs.2004.06.016 · Cited by 207 · see citing works

Meta-interpretive learning of higher-order dyadic datalog: predicate invention revisited

Muggleton, S. H., Lin, D., & Tamaddoni-Nezhad, A. (2015) · Machine Learning · doi:10.1007/s10994-014-5471-y · Cited by 184 · see citing works

Compiling with proofs

Necula, G. C., & Lee, P. (1998) · Cited by 174 · see citing works

Unification under a mixed prefix

Miller, D. (1992) · Journal of Symbolic Computation · doi:10.1016/0747-7171(92)90011-r · Cited by 166 · see citing works

Higher-order rewrite systems and their confluence

Mayr, R., & Nipkow, T. (1998) · Theoretical Computer Science · doi:10.1016/s0304-3975(97)00143-6 · Cited by 158 · see citing works

A proof theory for generic judgments

Miller, D., & Tiu, A. F. (2005) · ACM Transactions on Computational Logic · doi:10.1145/1094622.1094628 · Cited by 149 · see citing works

Dependently Typed Functional Programs and their Proofs

McBride, C. T. (2000) · ERA · Cited by 138 · see citing works

Isabelle/Isar --- a versatile environment for human-readable formal proof documents

Wenzel, M. (2002) · Cited by 133 · see citing works

Term-labeled categorial type systems

Oehrle, R. T. (1994) · Linguistics and Philosophy · doi:10.1007/bf00985321 · Cited by 127 · see citing works

Type classes: an exploration of the design space

Jones, S., Jones, M. P., & Meijer, E. (1997) · Cited by 121 · see citing works

Higher-order semantics and extensionality

Benzmüller, C., Brown, C. E., & Kohlhase, M. (2004) · Journal of Symbolic Logic · doi:10.2178/jsl/1102022211 · Cited by 108 · see citing works

Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)

Pientka, B., & Dunfield, J. (2010) · Lecture notes in computer science · doi:10.1007/978-3-642-14203-1_2 · Cited by 105 · see citing works

Higher-Order Unification and Matching

Gilles Dowek, B. (2001) · Elsevier eBooks · doi:10.1016/b978-044450813-3/50018-7 · Cited by 98 · see citing works

Efficient representation and validation of proofs

Necula, G. C., & Lee, P. (2002) · ACM/IEEE Symposium on Logic in Computer Science (LICS) · doi:10.1109/lics.1998.705646 · Cited by 97 · see citing works

Reasoning with higher-order abstract syntax in a logical framework

McDowell, R., & Miller, D. (2002) · ACM Transactions on Computational Logic · doi:10.1145/504077.504080 · Cited by 95 · see citing works

Oracle-based checking of untrusted software

Necula, G. C., & Rahul, S. P. (2001) · ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) · doi:10.1145/360204.360216 · Cited by 89 · see citing works

Elimination with a Motive

McBride, C. T. (2002) · Lecture notes in computer science · doi:10.1007/3-540-45842-5_13 · Cited by 88 · see citing works

Explaining type inference

Duggan, D., & Bent, F. (1996) · Science of Computer Programming · doi:10.1016/0167-6423(95)00007-0 · Cited by 83 · see citing works

Higher Order Unification via Explicit Substitutions

Gilles Dowek, B., Hardin, T., & Kirchner, C. (2000) · Information and Computation · doi:10.1006/inco.1999.2837 · Cited by 80 · see citing works

αProlog: A Logic Programming Language with Names, Binding and α-Equivalence

Cheney, J., & Urban, C. (2004) · Lecture notes in computer science · doi:10.1007/978-3-540-27775-0_19 · Cited by 78 · see citing works

Higher-order narrowing with definitional trees

Hanus, M., & Prehofer, C. (1999) · Journal of Functional Programming · doi:10.1017/s0956796899003330 · Cited by 75 · see citing works

Automating Open Bisimulation Checking for the Spi Calculus

Tiu, A. F., & Dawson, J. E. (2010) · IEEE Computer Security Foundations Workshop (CSFW) · doi:10.1109/csf.2010.28 · Cited by 74 · see citing works

Efficient resource management for linear logic proof search

Iliano Cervesato, A., Hodas, J. S., & Pfenning, F. (2000) · Theoretical Computer Science · doi:10.1016/s0304-3975(99)00173-5 · Cited by 73 · see citing works

Nominal logic programming

Cheney, J., & Urban, C. (2008) · ACM Transactions on Programming Languages and Systems · doi:10.1145/1387673.1387675 · Cited by 72 · see citing works

Sense and the Computation of Reference

Muskens, R. (2005) · Linguistics and Philosophy · doi:10.1007/s10988-004-7684-1 · Cited by 71 · see citing works

Programming with proofs and explicit contexts

Pientka, B., & Dunfield, J. (2008) · International Symposium on Principles and Practice of Declarative Programming (PPDP) · doi:10.1145/1389449.1389469 · Cited by 71 · see citing works

Unification via Explicit Substitutions: The Case of Higher-Order Patterns.

Gilles Dowek, B., Hardin, T., Kirchner, C., & Pfenning, F. (1996) · Cited by 69 · see citing works

Types for Modules

Russo, C. V. (2004) · Electronic Notes in Theoretical Computer Science · doi:10.1016/s1571-0661(05)82621-0 · Cited by 66 · see citing works

Implementing tactics and tacticals in a higher-order logic programming language

Felty, A. (1993) · Journal of Automated Reasoning · doi:10.1007/bf00881900 · Cited by 65 · see citing works

Inductive-data-type systems

Blanqui, F., Jouannaud, J.-P., & Okada, M. (2002) · Theoretical Computer Science · doi:10.1016/s0304-3975(00)00347-9 · Cited by 63 · see citing works

Logical calculi for reasoning with binding

Mathijssen, A. (2007) · TU/e Research Portal · doi:10.6100/ir630460 · Cited by 62 · see citing works

Isabelle/Isar — a Generic Framework for Human-Readable Proof Documents

Wenzel, M. (2007) · Cited by 61 · see citing works

Ordered linear logic and applications

Polakow, J., & Pfenning, F. (2001) · Cited by 60 · see citing works

A proof theory for generic judgments: an extended abstract

Miller, D., & Tiu, A. F. (2003) · ACM/IEEE Symposium on Logic in Computer Science (LICS) · doi:10.1109/lics.2003.1210051 · Cited by 60 · see citing works

Developing developments

van Oostrom, V. (1997) · Theoretical Computer Science · doi:10.1016/s0304-3975(96)00173-9 · Cited by 59 · see citing works

Linear second-order unification

Levy, J. (1996) · Lecture notes in computer science · doi:10.1007/3-540-61464-8_63 · Cited by 59 · see citing works

Functional and Constraint Logic Programming

Rodríguez-Artalejo, M. (2001) · Lecture notes in computer science · doi:10.1007/3-540-45406-3_5 · Cited by 58 · see citing works

A Coverage Checking Algorithm for LF

Schürmann, C., & Pfenning, F. (2003) · Lecture notes in computer science · doi:10.1007/10930755_8 · Cited by 58 · see citing works

Proof Theory at Work: Program Development in the Minlog System

Benl, Berger, Schwichtenberg, Seisenberger, & Zuber (1998) · Applied logic series · doi:10.1007/978-94-017-0435-9_2 · Cited by 57 · see citing works

Proof Terms for Simply Typed Higher Order Logic

Berghofer, S., & Nipkow, T. (2000) · Lecture notes in computer science · doi:10.1007/3-540-44659-1_3 · Cited by 57 · see citing works

Logical Frameworks

Pfenning, F. (2001) · Elsevier eBooks · doi:10.1016/b978-044450813-3/50019-9 · Cited by 57 · see citing works

Automation of Higher-Order Logic

Benzmüller, C., & Miller, D. (2014) · Handbook of the history of logic · doi:10.1016/b978-0-444-51624-4.50005-8 · Cited by 55 · see citing works

Polymorphic higher-order recursive path orderings

Jouannaud, J.-P., & Rubio, A. (2007) · Journal of the ACM · doi:10.1145/1206035.1206037 · Cited by 54 · see citing works

Monadic concurrent linear logic programming

López, P., Pfenning, F., Polakow, J., & Watkins, K. (2005) · International Symposium on Principles and Practice of Declarative Programming (PPDP) · doi:10.1145/1069774.1069778 · Cited by 50 · see citing works

Abstract Syntax for Variable Binders: An Overview

Miller, D. (2000) · Lecture notes in computer science · doi:10.1007/3-540-44957-4_16 · Cited by 50 · see citing works

Mode and termination checking for higher-order logic programs

Rohwedder, E., & Pfenning, F. (1996) · Lecture notes in computer science · doi:10.1007/3-540-61055-3_44 · Cited by 47 · see citing works

A logic for reasoning with higher-order abstract syntax

McDowell, R., & Miller, D. (2002) · ACM/IEEE Symposium on Logic in Computer Science (LICS) · doi:10.1109/lics.1997.614968 · Cited by 47 · see citing works

Combining Generic Judgments with Recursive Definitions

Gacek, A., Miller, D., & Nadathur, G. (2008) · ACM/IEEE Symposium on Logic in Computer Science (LICS) · doi:10.1109/lics.2008.33 · Cited by 46 · see citing works

Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL

Lachnitt, H., Fleury, M., Barbosa, H., Jakpor, J. Z., Andreotti, B., Reynolds, A., Schurr, H.-J., Barrett, C., & Tinelli, C. (2025) · Leibniz international proceedings in informatics · doi:10.4230/lipics.itp.2025.26 · Cited by 44 · see citing works

TPS: A hybrid automatic-interactive system for developing proofs

Andrews, P. B., & Brown, C. E. (2005) · Journal of Applied Logic · doi:10.1016/j.jal.2005.10.002 · Cited by 44 · see citing works

A proof procedure for the logic of hereditary Harrop formulas

Nadathur, G. (1993) · Journal of Automated Reasoning · doi:10.1007/bf00881902 · Cited by 44 · see citing works

A theory of binding structures and applications to rewriting

Talcott, C. (1993) · Theoretical Computer Science · doi:10.1016/0304-3975(93)90240-t · Cited by 43 · see citing works

The practice of logical frameworks

Pfenning, F. (1996) · Lecture notes in computer science · doi:10.1007/3-540-61064-2_33 · Cited by 41 · see citing works

ELPI: Fast, Embeddable, $$\lambda $$ Prolog Interpreter

Dunchev, C., Guidi, F., Coen, C. S., & Tassi, E. (2015) · Lecture notes in computer science · doi:10.1007/978-3-662-48899-7_32 · Cited by 38 · see citing works

Foundational aspects of syntax

Miller, D., & Catuscia Palamidessi, A. (1999) · ACM Computing Surveys · doi:10.1145/333580.333590 · Cited by 36 · see citing works

Higher-order matching for program transformation

de Moor, O., & Sittampalam, G. (2001) · Theoretical Computer Science · doi:10.1016/s0304-3975(00)00402-3 · Cited by 36 · see citing works

Higher Order Unification and the Interpretation of Focus

Pulman, S. (1997) · Linguistics and Philosophy · doi:10.1023/a:1005394619746 · Cited by 36 · see citing works

Outrageous but meaningful coincidences

McBride, C. T. (2010) · Workshop on Generic Programming · doi:10.1145/1863495.1863497 · Cited by 34 · see citing works

Open Proofs and Open Terms: A Basis for Interactive Logic

Geuvers, H., & Jojgov, G. (2002) · Lecture notes in computer science · doi:10.1007/3-540-45793-3_36 · Cited by 34 · see citing works

Nominal Unification from a Higher-Order Perspective

Levy, J., & Villaret, M. (2008) · Lecture notes in computer science · doi:10.1007/978-3-540-70590-1_17 · Cited by 33 · see citing works

Top-Down Synthesis for Library Learning

Bowers, M., Olausson, T. X., Wong, L., Grand, G., Tenenbaum, J. B., Ellis, K., & Solar-Lezama, A. (2023) · Proceedings of the ACM on Programming Languages · doi:10.1145/3571234 · Cited by 33 · see citing works

A polynomial nominal unification algorithm

Calvès, C., & Fernández, M. (2008) · Theoretical Computer Science · doi:10.1016/j.tcs.2008.05.012 · Cited by 33 · see citing works

A Logic for Reasoning about Generic Judgments

Tiu, A. F. (2007) · Electronic Notes in Theoretical Computer Science · doi:10.1016/j.entcs.2007.01.016 · Cited by 32 · see citing works

Reasoning in a logic with definitions and induction

McDowell, R., & Miller, D. (1997) · Scholarly Commons (University of Pennsylvania) · Cited by 32 · see citing works

Negative polarity licensing at the syntax-semantics interface

Fry, J. B. (1997) · Conference of the European Chapter of the Association for Computational Linguistics · doi:10.3115/979617.979636 · Cited by 31 · see citing works

A Proof Search Specification of the π-Calculus

Tiu, A. F., & Miller, D. (2005) · Electronic Notes in Theoretical Computer Science · doi:10.1016/j.entcs.2005.05.006 · Cited by 31 · see citing works

Generic Automatic Proof ToolsPreprint

Paulson, L. C. (2001) · arXiv (Cornell University) · doi:10.48550/arxiv.cs/9711106 · Cited by 31 · see citing works

The Complexity of Equivariant Unification

Cheney, J. (2004) · Lecture notes in computer science · doi:10.1007/978-3-540-27836-8_30 · Cited by 30 · see citing works

Extending definite clause grammars with scoping constructs

Pareschi, R., & Miller, D. (1990) · Cited by 30 · see citing works

On the algebraic structure of declarative programming languages

Amato, G., Lipton, J., & McGrail, R. W. (2009) · Theoretical Computer Science · doi:10.1016/j.tcs.2009.07.038 · Cited by 29 · see citing works

Nominal Unification from a Higher-Order Perspective

Levy, J., & Villaret, M. (2012) · ACM Transactions on Computational Logic · doi:10.1145/2159531.2159532 · Cited by 29 · see citing works

Typed Higher-Order Narrowing without Higher-Order Strategies

Antoy, S., & Tolmach, A. P. (1999) · Lecture notes in computer science · doi:10.1007/10705424_22 · Cited by 29 · see citing works

Higher-Order Logic Programming

Nadathur, G., & Miller, D. (1998) · Oxford University Press eBooks · doi:10.1093/oso/9780198537922.003.0011 · Cited by 29 · see citing works

Higher-order annotated terms for proof search

Smaill, A., & Green, I. (1996) · Lecture notes in computer science · doi:10.1007/bfb0105418 · Cited by 29 · see citing works

Proof search specifications of bisimulation and modal logics for the π-calculus

Tiu, A. F., & Miller, D. (2010) · ACM Transactions on Computational Logic · doi:10.1145/1656242.1656248 · Cited by 28 · see citing works

A fully adequate shallow embedding of the π-calculus in Isabelle/HOL with mechanized syntax analysis

Röckl, C., & Hirschkoff, D. (2003) · Journal of Functional Programming · doi:10.1017/s0956796802004653 · Cited by 28 · see citing works

Rewriting Calculus with(out) Types

Cirstea, H., Kirchner, C., & Liquori, L. (2004) · Electronic Notes in Theoretical Computer Science · doi:10.1016/s1571-0661(05)82526-5 · Cited by 28 · see citing works

Extended natural semantics

Hannan, J. (1993) · Journal of Functional Programming · doi:10.1017/s0956796800000666 · Cited by 27 · see citing works

Higher-Order Rewriting

van Raamsdonk, F. (1999) · Lecture notes in computer science · doi:10.1007/3-540-48685-2_17 · Cited by 26 · see citing works

Higher-order families

van Oostrom, V. (1996) · Lecture notes in computer science · doi:10.1007/3-540-61464-8_67 · Cited by 26 · see citing works

Middle-Out Reasoning for Logic Program Synthesis

Kraan, I., Basin, D., & Bundy, A. (1993) · Edinburgh Research Explorer (University of Edinburgh) · Cited by 26 · see citing works

Extensional Higher-Order Paramodulation in Leo-III

Steen, A., & Benzmüller, C. (2021) · Journal of Automated Reasoning · doi:10.1007/s10817-021-09588-x · Cited by 25 · see citing works

Rewriting and call-time choice: the HO case

López-Fraguas, F. J., Rodríguez-Hortalá, J., & Sánchez-Hernández, J. (2008) · Docta Complutense (Universidad Complutense de Madrid) · doi:10.5555/1788446.1788463 · Cited by 25 · see citing works

Minlog - A Tool for Program Extraction Supporting Algebras and Coalgebras

Berger, U., Miyamoto, K., Schwichtenberg, H., & Seisenberger, M. (2011) · Lecture notes in computer science · doi:10.1007/978-3-642-22944-2_29 · Cited by 25 · see citing works

Linear unification of higher-order patterns

Qian, Z. (1993) · Lecture notes in computer science · doi:10.1007/3-540-56610-4_78 · Cited by 25 · see citing works

A finitary version of the calculus of partial inductive definitions

Eriksson, L.-H. (2005) · Springer eBooks · doi:10.1007/bfb0013605 · Cited by 25 · see citing works

On Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems

Sakai, M. (2005) · IEICE Transactions on Information and Systems · doi:10.1093/ietisy/e88-d.3.583 · Cited by 25 · see citing works

The HOL Light manual (1.1)

Harrison, J. (2000) · Cited by 25 · see citing works

Superposition with Lambdas

Bentkamp, A., Blanchette, J. C., Tourret, S., Vukmirović, P., & Waldmann, U. (2019) · Lecture notes in computer science · doi:10.1007/978-3-030-29436-6_4 · Cited by 24 · see citing works

Matching and alpha-equivalence check for nominal terms

Calvès, C., & Fernández, M. (2009) · Journal of Computer and System Sciences · doi:10.1016/j.jcss.2009.10.003 · Cited by 24 · see citing works

Higher-order constraint simplification in dependent type theory

Reed, J. (2009) · International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP) · doi:10.1145/1577824.1577832 · Cited by 24 · see citing works

Higher-order narrowing with definitional trees

Hanus, M., & Prehofer, C. (1996) · Lecture notes in computer science · doi:10.1007/3-540-61464-8_48 · Cited by 24 · see citing works

Nominal Renaming Sets

Gabbay, M. J., & Hofmann, M. (2008) · Lecture notes in computer science · doi:10.1007/978-3-540-89439-1_11 · Cited by 23 · see citing works

Cut elimination for a logic with induction and co-induction

Tiu, A. F., & Momigliano, A. (2012) · Journal of Applied Logic · doi:10.1016/j.jal.2012.07.007 · Cited by 23 · see citing works

Algorithms for Equality and Unification in the Presence of Notational Definitions

Pfenning, F., & Schürmann, C. (1999) · Lecture notes in computer science · doi:10.1007/3-540-48167-2_13 · Cited by 23 · see citing works

A Logic Programming Language with Lambda-Abstraction, Function Vari- ables, and Simple Unification," in Extensions of Logic Programming edited b y Peter Schroeder

Miller, D. (1990)

Unification of Simply Typed Lambda-Terms as Logic Programming

Miller, D. (1991) · ScholarlyCommons (University of Pennsylvania) · Cited by 69 · see citing works

An overview of lProlog

Nadathur, G., Miller, D., Nadathur, G., Lambda-prolog, A. O. O., Nadathur, G., & Lab, L. (1988)

An Overview of λProlog

Nadathur, G., & Miller, D. (1988)

Predicate abstractions in higher-order logic programming

Chen, W., & Warren, D. S. (1996) · New Generation Computing · doi:10.1007/bf03037499