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

MILLER, DALE·1991·Journal of Logic and Computation
DOI 10.1093/logcom/1.4.497

Cited by (380)

Items 101–200 of 380

  1. Nominal Unification
    Christian Urban, Andrew M. Pitts, Murdoch J. Gabbay · 2003 · Lecture notes in computer science
  2. A termination ordering for higher order rewrite systems
    Olav Lysne, Javier Piris · 1995 · Lecture notes in computer science
  3. Combining Higher-Order and First-Order Computation Using Rho Calculus: Towards a Semantics of ELAN
    Horatiu Cirstea, Claude Kirchner · 1998
  4. CSI: New Evidence – A Progress Report
    Julian Nagele, Bertram Felgenhauer, Aart Middeldorp · 2017 · Lecture notes in computer science
  5. Case Analysis of Higher-Order Data
    Jana Dunfield, Brigitte Pientka · 2009 · Electronic Notes in Theoretical Computer Science
  6. Abstract syntax and logic programming
    Dale Miller · 1992 · Lecture notes in computer science
  7. Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques
    Gilles Dowek B, Murdoch J. Gabbay, Dominic P. Mulligan · 2010 · Logic Journal of IGPL
  8. Finite family developments
    Vincent van Oostrom · 1997 · Lecture notes in computer science
  9. Relating Nominal and Higher-Order Pattern Unification
    James Cheney · 2005
  10. Construction and deduction in type theories
    Martin Strecker · 1999 · OPen Access Repositorium der Universität Ulm (OPARU) (Ulm University)
  11. A Nominal Axiomatization of the Lambda Calculus
    Murdoch J. Gabbay, Aad Mathijssen · 2009 · Journal of Logic and Computation
  12. Complexity of the Higher Order Matching
    ToMasz Wierzbicki · 1999 · Lecture notes in computer science
  13. On Termination of Higher-Order Rewriting
    Femke van Raamsdonk · 2001 · Lecture notes in computer science
  14. A hybrid logical framework
    Frank Pfenning, Jason Reed · 2009
  15. Permissive nominal terms and their unication
    Gilles Dowek B, Murdoch J. Gabbay, Dominic P. Mulligan · 2009
  16. Nominal Unification of Higher Order Expressions with Recursive Let
    Manfred Schmidt-Schauß, Temur Kutsia, Jordi Levy, Mateu Villaret · 2017 · Lecture notes in computer science
  17. Proof Generation in the Touchstone Theorem Prover
    George C. Necula, Peter Lee · 2000 · Lecture notes in computer science
  18. Fully Automatic Adaptation of Software Components Based on Semantic Specifications*
    Christian Haack, Brian Howard, Allen Stoughton, J. B. Wells · 2002 · Lecture notes in computer science
  19. Proofs, Programs and Executable Specifications in Higher Order Logic
    Stefan Berghofer · 2003
  20. A logic programming approach to implementing higher-Order term rewriting
    Amy Felty · 2005 · Springer eBooks
  21. Term rewriting with variable binding
    Makoto Hamana · 2003 · International Symposium on Principles and Practice of Declarative Programming (PPDP)
  22. Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions
    Amy Felty, Alberto Momigliano, Brigitte Pientka · 2017 · Mathematical Structures in Computer Science
  23. Higher-Order Orderings for Normal Rewriting
    Jean-Pierre Jouannaud, Albert Rubio · 2006 · Lecture notes in computer science
  24. Choices in Representation and Reduction Strategies for Lambda Terms in Intensional Contexts
    Chuck C. Liang, Gopalan Nadathur, Xiaochu Qi · 2004 · Journal of Automated Reasoning
  25. Program Development by Proof Transformation
    Ulrich Berger, Helmut Schwichtenberg · 1995 · Springer eBooks
  26. Higher-Order Pattern Anti-Unification in Linear Time
    Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret · 2016 · Journal of Automated Reasoning
  27. Uniform provability in classical logic
    Gopalan Nadathur · 1998 · Journal of Logic and Computation
  28. PlinyCompute
    Jia Zou, R. Matthew Barnett, Tania Lorido-Botrán, Shangyu Luo, Carlos Rodríguez Monroy, Sourav Sikdar, Kia Teymourian, Binhang Yuan, Chris Jermaine · 2018 · ACM SIGMOD International Conference on Management of Data (SIGMOD)
  29. Higher-order term indexing using substitution trees
    Brigitte Pientka · 2009 · ACM Transactions on Computational Logic
  30. The calculus of nominal inductive constructions
    Edwin Westbrook, Aaron Stump, Evan Austin · 2009 · International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP)
  31. Towards Inductive Generalisation in Higher Order Logic
    Feng Cao, Stephen Muggleton · 1992 · Elsevier eBooks
  32. Oracle-based checking of untrusted software
    George C. Necula, Shree P. Rahul · 2001 · ACM SIGPLAN Notices
  33. Redundancy Elimination for LF
    Jason Reed · 2008 · Electronic Notes in Theoretical Computer Science
  34. Hiord: A Type-Free Higher-Order Logic Programming Language with Predicate Abstraction
    Daniel Cabeza, Manuel V. Hermenegildo, James Lipton · 2004 · Lecture notes in computer science
  35. On implicit arguments
    Masami Hagiya, Yozo Toda · 2005 · Springer eBooks
  36. A Methodological View of Constraint Solving
    Hubert Comon, Mehmet Dincbas, Jean-Pierre Jouannaud, Claude Kirchner · 1999 · Constraints
  37. A Proof-Theoretic Framework for Logic Programming
    Gerhard Jäger, Robert F. Stärk · 1998 · Studies in logic and the foundations of mathematics
  38. Equivalence of Reductions in Higher-Order Rewriting
    H. J. Sander Bruggink · 2008 · Utrecht University Repository (Utrecht University)
  39. Termination of rewrite relations on λ-terms based on Girard's notion of reducibility
    Frédéric Blanqui · 2015 · Theoretical Computer Science
  40. An Improved Extensionality Criterion for Higher-Order Logic Programs
    Marc Bezem · 2001 · Lecture notes in computer science
  41. How to prove your calculus is decidable: practical applications of second-order algebraic theories and computation
    Makoto Hamana · 2017 · Proceedings of the ACM on Programming Languages
  42. The CADE-26 automated theorem proving system competition – CASC-26
    Geoff Sutcliffe · 2017 · AI Communications
  43. Superposition with Lambdas
    Alexander Bentkamp, Jasmin Christian Blanchette, Sophie Tourret, Petar Vukmirović, Uwe Waldmann · 2021 · Journal of Automated Reasoning
  44. Mixing Finite Success and Finite Failure in an Automated Prover
    Alwen Fernanto Tiu, Gopalan Nadathur, Dale Miller · 2005
  45. Practical Higher-Order Pattern Unification with On-the-Fly Raising
    Gopalan Nadathur, Natalie Linnell · 2005 · Lecture notes in computer science
  46. Deterministic second-order patterns
    Tetsuo Yokoyama, Zhenjiang Hu, Masato Takeichi · 2004 · Information Processing Letters
  47. A Logic Programming Language Based on Binding Algebras
    Makoto Hamana · 2001 · Lecture notes in computer science
  48. Higher-Order Rewriting: Framework, Confluence and Termination
    Jean-Pierre Jouannaud · 2005 · Lecture notes in computer science
  49. The First-Order Nominal Link
    Christophe Calvès, Maribel Fernández · 2011 · Lecture notes in computer science
  50. Nominal Unification Revisited
    Christian Urban · 2010 · Electronic Proceedings in Theoretical Computer Science
  51. Representing and Reasoning with Operational Semantics
    Dale Miller · 2006 · Lecture notes in computer science
  52. Rewriting and Call-Time Choice: The HO Case
    Francisco J. López-Fraguas, Juan Rodríguez-Hortalá, Jaime Sánchez-Hernández · 2008 · Springer eBooks
  53. Functional Logic Programming with Distributed Constraint Solving
    Mircea Marin · 2000
  54. Linear Higher-Order Matching Is NP-Complete
    Philippe de Groote · 2000 · Lecture notes in computer science
  55. Uniform proofs and disjunctive logic programming
    Gopalan Nadathur, Donald W. Loveland · 2002 · ACM/IEEE Symposium on Logic in Computer Science (LICS)
  56. Tradeoffs in the Intensional Representation of Lambda Terms
    Chuck C. Liang, Gopalan Nadathur · 2002 · Lecture notes in computer science
  57. Compiler Construction in Higher Order Logic Programming
    Chuck C. Liang · 2001 · Lecture notes in computer science
  58. A Variant of Higher-Order Anti-Unification
    Baumgartner, Alexander, Temur Kutsia, Jordi Levy, Mateu Villaret · 2013 · LA Referencia (Red Federada de Repositorios Institucionales de Publicaciones Científicas)
  59. Logic programming and logic grammars with first-order continuations
    Paul Tarau, Verónica Dahl · 1994 · Lecture notes in computer science
  60. Outermost-fair rewriting
    Femke van Raamsdonk · 1997 · Lecture notes in computer science
  61. Higher-Order Logic Programming as Constraint Logic Programming.
    Spiro Michaylov, Frank Pfenning · 1993
  62. Generic Proof Tools and Finite Group Theory
    François Garillot · 2011 · OpenGrey (Institut de l'Information Scientifique et Technique)
  63. Design and implementation of practical constraint logic programming systems
    Spiro Michaylov · 1992 · Defense Technical Information Center (DTIC)
  64. Abstract Syntax and Logic Programming.
    Dale Miller · 1991
  65. Universal algebra over lambda-terms and nominal terms
    Murdoch J. Gabbay, Dominic P. Mulligan · 2009 · International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP)
  66. A meta-programming approach to realizing dependently typed logic programming
    Zachary Snow, David Baelde, Gopalan Nadathur · 2010 · International Symposium on Principles and Practice of Declarative Programming (PPDP)
  67. From context-free to definite-clause grammars: a type-theoretic approach
    Juergen Haas, Bharat Jayaraman · 1997 · The Journal of Logic Programming
  68. Decidability of Arity-Bounded Higher-Order Matching
    Manfred Schmidt-Schauß · 2003 · Lecture notes in computer science
  69. A treatment of higher-order features in logic programming
    Gopalan Nadathur · 2005 · Theory and Practice of Logic Programming
  70. X.R.S: Explicit reduction systems — A first-order calculus for higher-order calculi
    Bruno Pagano · 1998 · Lecture notes in computer science
  71. Managing Structural Information by Higher-Order Colored Unification
    Dieter Hutter, Michael Kohlhase · 2000 · Journal of Automated Reasoning
  72. Higher-order equational logic programming
    Zhenyu Qian · 1994 · ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)
  73. How to prove decidability of equational theories with second-order computation analyser SOL
    Makoto Hamana · 2019 · Journal of Functional Programming
  74. Computability Closure: Ten Years Later
    Frédéric Blanqui · 2007 · Lecture notes in computer science
  75. Minimal from classical proofs
    Helmut Schwichtenberg, Christoph-Simon Senjak · 2012 · Annals of Pure and Applied Logic
  76. A Rewrite System for Proof Constructivization
    Raphaël Cauderlier · 2016
  77. Encoding Generic Judgments
    Dale Miller, Alwen Fernanto Tiu · 2002 · Lecture notes in computer science
  78. Decidability of Bounded Higher-Order Unification
    Manfred Schmidt-Schauß, Klaus U. Schulz · 2002 · Lecture notes in computer science
  79. The Suspension Notation for Lambda Terms and its Use in Metalanguage Implementations
    Gopalan Nadathur · 2002 · Electronic Notes in Theoretical Computer Science
  80. Higher-Order Positive Set Constraints
    Jean Goubault-Larrecq · 2002 · Lecture notes in computer science
  81. Program derivation by proof transformation
    Penny Anderson · 1993 · Defense Technical Information Center (DTIC)
  82. Correspondences between classical, intuitionistic and uniform provability
    Gopalan Nadathur · 2000 · Theoretical Computer Science
  83. Modular AC unification of higher-order patterns
    Zhenyu Cheryl Qian, Kang Wang · 2005 · Springer eBooks
  84. Mechanized Metatheory Revisited
    Dale Miller · 2018 · Journal of Automated Reasoning
  85. PNL to HOL: From the logic of nominal sets to the logic of higher-order functions
    Gilles Dowek B, Murdoch J. Gabbay · 2012 · Theoretical Computer Science
  86. Undecidability of higher-order unification formalised in Coq
    Simon Spies, Yannick Forster · 2020 · ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP)
  87. A Survey of the Proof-Theoretic Foundations of Logic Programming
    Dale Miller · 2021 · Theory and Practice of Logic Programming
  88. Pattern Unification for the Lambda Calculus with Linear and Affine Types
    Anders Schack-Nielsen, Carsten Schürmann · 2010 · Electronic Proceedings in Theoretical Computer Science
  89. Idempotent Anti-unification
    David M. Cerna, Temur Kutsia · 2019 · ACM Transactions on Computational Logic
  90. Higher-order encodings with constructors
    Robert B. Pless, Edwin M. Westbrook · 2008
  91. Extending Higher-Order Unification to Support Proof Irrelevance
    Jason Reed · 2003 · Lecture notes in computer science
  92. Object calculi in linear logic
    Michele Bugliesi A · 2000 · Journal of Logic and Computation
  93. Unification with extended patterns
    Dominic Duggan · 1998 · Theoretical Computer Science
  94. The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations: Part 1-A Common Infrastructure for Benchmarks
    Amy Felty, Alberto Momigliano, Brigitte Pientka · 2015 · arXiv (Cornell University)
  95. Higher-Order Pattern Matching for Automatically Applying Fusion Transformations
    Ganesh Sittampalam, Oege de Moor · 2001 · Lecture notes in computer science
  96. Tractable and Intractable Second-Order Matching Problems
    Kouichi Hirata, Keizo Yamada, Masateru Harao · 1999 · Lecture notes in computer science
  97. Decidability of bounded higher-order unification
    Manfred Schmidt-Schauß, Klaus U. Schulz · 2005 · Journal of Symbolic Computation
  98. More On Implicit Syntax
    Marko Luther · 2001 · Lecture notes in computer science
  99. A Library of Anti-unification Algorithms
    Alexander Baumgartner, Temur Kutsia · 2014 · Lecture notes in computer science
  100. Higher-Order Quantification and Proof Search*
    Dale Miller · 2002 · Lecture notes in computer science