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 201–300 of 380

  1. A Termination Ordering for Higher Order Rewrite System
    Olav Lysne, Javier Piris · 1995 · Rewriting Techniques and Applications
  2. A semantics for λProlog
    D. A. Wolfram · 1994 · Theoretical Computer Science
  3. Higher-order pattern complement and the strict λ-calculus
    Alberto Momigliano, Frank Pfenning · 2003 · ACM Transactions on Computational Logic
  4. Negative polarity licensing at the syntax-semantics interface
    J. B. Fry · 1997 · Proceedings of the conference - Association for Computational Linguistics. Meeting
  5. Church-Rosser Properties of Normal Rewriting
    Jean-Pierre Jouannaud, Li, Jianqi · 2012 · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics)
  6. A Higher-Order Demand-Driven Narrowing Calculus with Definitional Trees
    Rafael del Vado Vírseda · 2007 · Lecture notes in computer science
  7. Let-polymorphism and eager type schemes
    Chuck C. Liang · 1997 · Lecture notes in computer science
  8. The graph rewriting calculus (properties and expressive capabilities)
    Clara Bertolissi, Claude Kirchner · 2005 · Publications Et Travaux Academiques de Lorraine (Universite de Lorraine)
  9. Polymorphic computation systems: Theory and practice of confluence with call-by-value
    Makoto Hamana, Tatsuya Abe, Kentaro Kikuchi · 2019 · Science of Computer Programming
  10. Polymorphic Session Processes as Morphisms
    Bernardo Toninho, Nobuko Yoshida · 2019 · Lecture notes in computer science
  11. Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract)
    Zakaria Chihani, Dale Miller, Fabien Renaud · 2018 · EPiC series in computing
  12. Polymorphic Rewrite Rules: Confluence, Type Inference, and Instance Validation
    Makoto Hamana · 2018 · Lecture notes in computer science
  13. Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs
    Gilles Dowek B, Gaspard Férey, Jean-Pierre Jouannaud, Jiaxiang Liu · 2022 · Mathematical Structures in Computer Science
  14. Encoding Generic Judgments
    Dale Miller · 2001 · Electronic Notes in Theoretical Computer Science
  15. Deterministic Higher-Order Patterns for Program Transformation
    Tetsuo Yokoyama, Zhenjiang Hu, Masato Takeichi · 2004 · Lecture notes in computer science
  16. A language for the logical specification of processes and relations
    Luı́s Caires · 1996 · Lecture notes in computer science
  17. Towards the uniform implementation of declarative languages
    Manuel M. T. Chakravarty, Hendrik C. R. Lock · 1997 · Computer Languages
  18. A higher-order logical framework for the algorithmic debugging and verification of declarative programs
    Rafael del Vado Vírseda · 2009 · International Symposium on Principles and Practice of Declarative Programming (PPDP)
  19. Implementing type theory in higher order constraint logic programming
    Ferruccio Guidi, Claudio Sacerdoti Coen, ENRICO TASSI · 2019 · Mathematical Structures in Computer Science
  20. Elaboration with first-class implicit function types
    András Kovács · 2020 · Proceedings of the ACM on Programming Languages
  21. Higher-order pattern generalization modulo equational theories
    David M. Cerna, Temur Kutsia · 2020 · Mathematical Structures in Computer Science
  22. Nominal Unification and Matching of Higher Order Expressions with Recursive Let
    Manfred Schmidt-Schauß, Temur Kutsia, Jordi Levy, Mateu Villaret, Yunus Kutz · 2022 · Fundamenta Informaticae
  23. Safe, fast, concurrent proof checking for the lambda-pi calculus modulo rewriting
    Michael Färber · 2022 · ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP)
  24. The Isabelle/Isar Implementation
    Makarius Wenzel, Stefan Berghofer, Florian Haftmann, Lawrence Charles Paulson, Andrew S. Tanenbaum, Brian W. Kernighan, Alan C. Kay · 2016
  25. Expressing combinatory reduction systems derivations in the rewriting calculus
    Clara Bertolissi, Horatiu Cirstea, Claude Kirchner · 2006 · LISP and Symbolic Computation
  26. An initial algebra approach to term rewriting systems with variable binders
    Makoto Hamana · 2006 · LISP and Symbolic Computation
  27. Logical approximation for program analysis
    Robert J. Simmons, Frank Pfenning · 2011 · LISP and Symbolic Computation
  28. Reduction and unification in lambda calculi with a general notion of subtype
    Zhenyu Qian, Tobias Nipkow · 1994 · Journal of Automated Reasoning
  29. Explicit substitutions in the reduction of lambda terms
    Gopalan Nadathur, Xiaochu Qi · 2003 · International Symposium on Principles and Practice of Declarative Programming (PPDP)
  30. Introduction to Milestones in Interactive Theorem Proving
    Jeremy D. Avigad, Jasmin Christian Blanchette, Gerwin Klein, Lawrence Charles Paulson, Andrei Popescu, Gregor Snelting · 2018 · Journal of Automated Reasoning
  31. CLP(H):Constraint logic programming for hedges
    Besik Dundua, Mário Florido, Temur Kutsia, Mircea Marin · 2015 · Theory and Practice of Logic Programming
  32. The Metalanguage λprolog and Its Implementation
    Gopalan Nadathur · 2001 · Lecture notes in computer science
  33. A strategy for dynamic interpretation
    Olivier Bouchez, Jan van Eijck, Olivier Istace · 1993 · Conference of the European Chapter of the Association for Computational Linguistics
  34. Investigation on the typing of equality in type systems
    Vincent Siles · 2010 · OpenGrey (Institut de l'Information Scientifique et Technique)
  35. A Static Higher-Order Dependency Pair Framework
    Carsten Fuhs, Cynthia Kop · 2019 · Lecture notes in computer science
  36. Functions-as-constructors higher-order unification: extended pattern unification
    Tomer Libal, Dale Miller · 2021 · Annals of Mathematics and Artificial Intelligence
  37. A Hypersequent System for Gödel-Dummett Logic with Non-constant Domains
    Alwen Fernanto Tiu · 2011 · Lecture notes in computer science
  38. Tactics and Certificates in Meta Dedukti
    Raphaël Cauderlier · 2018 · Lecture notes in computer science
  39. Adelfa: A System for Reasoning about LF Specifications
    Mary Southern, Gopalan Nadathur · 2021 · Electronic Proceedings in Theoretical Computer Science
  40. Higher Order Matching for Program Transformation
    Oege de Moor, Ganesh Sittampalam · 1999 · Lecture notes in computer science
  41. Optimizing the Runtime Processing of Types in Polymorphic Logic Programming Languages
    Gopalan Nadathur, Xiaochu Qi · 2005 · Lecture notes in computer science
  42. A proof-theoretic treatment of λ-reduction with cut-elimination: λ-calculus as a logic programming language
    Michael Gabbay · 2011 · Journal of Symbolic Logic
  43. Hobbits for Haskell
    Edwin Westbrook, Nicolas Frisby, Paul Brauner · 2011
  44. Functional Programming With Higher-order Abstract Syntax and Explicit Substitutions
    Brigitte Pientka · 2007 · Electronic Notes in Theoretical Computer Science
  45. Normal Higher-Order Termination
    Jean-Pierre Jouannaud, Albert Rubio · 2015 · ACM Transactions on Computational Logic
  46. Residuals in Higher-Order Rewriting
    H. J. Sander Bruggink · 2003 · Lecture notes in computer science
  47. Property-Based Testing via Proof Reconstruction
    Roberto Blanco, Dale Miller, Alberto Momigliano · 2019 · International Symposium on Principles and Practice of Declarative Programming (PPDP)
  48. Revisiting Graph Types in HyperLMNtal: A Modeling Language for Hypergraph Rewriting
    Alimujiang Yasen, Kazunori Ueda · 2021 · IEEE Access
  49. Matching Modulo Superdevelopments Application to Second-Order Matching
    Germain Faure · 2006 · Lecture notes in computer science
  50. On introducing higher order functions in ABEL
    Bjørn Kristoffersen, Ole-Johan Dahl · 1998
  51. An Implementation of the Language Lambda Prolog Organized around Higher-Order Pattern Unification
    Qi, Xiaochu · 2009 · arXiv (Cornell University)
  52. The Metalanguage lambda-Prolog and Its Implementation
    Gopalan Nadathur · 2001 · International Symposium on Functional and Logic Programming
  53. A Comparative Study between the Direct and Overheard Speech of Primary Caregiver of Late Talkers and Typically Developing Infants
    Jiyeon Lee, Dongsun Yim · 2017 · Eon'eo cheong'gag jang'ae yeon'gu/Communication sciences & disorders
  54. Term Evaluation Systems with Refinements: First-Order, Second-Order, and Contextual Improvement
    Koko Muroya, Makoto Hamana · 2024 · Lecture notes in computer science
  55. Algorithms for Equality and Unification in the Presence of Notational Definitions
    Frank Pfenning, Carsten Schürmann · 1998 · Electronic Notes in Theoretical Computer Science
  56. A domain model characterising strong normalisation
    Ulrich Berger · 2008 · Annals of Pure and Applied Logic
  57. Generalization Algorithms for Second-Order Terms
    Kouichi Hirata, Takeshi Ogawa, Masateru Harao · 2004 · Lecture notes in computer science
  58. Implementing Substructural Logical Frameworks
    Anders Schack-Nielsen · 2011
  59. Confluence in Non-Left-Linear Untyped Higher-Order Rewrite Theories
    Gaspard Férey, Jean-Pierre Jouannaud · 2021 · International Symposium on Principles and Practice of Declarative Programming (PPDP)
  60. Australian National University
    Alwen Tiu, Dale Miller, Cedex France · 1960 · Anthropology News
  61. Stratification in Logics of Definitions
    Alwen Fernanto Tiu · 2012 · Lecture notes in computer science
  62. A Theoretical Framework for the Declarative Debugging of Functional Logic Programs with Lambda Abstractions
    Rafael del Vado Vírseda, Ignacio Castiñeiras · 2010 · Lecture notes in computer science
  63. About the confluence of equational pattern rewrite systems
    Alexandre Boudet, Évelyne Contejean · 1998 · Lecture notes in computer science
  64. Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type
    Roland Fettig, Bernd Löchner · 1996 · Lecture notes in computer science
  65. A Proof of Finite Family Developments for Higher-Order Rewriting Using a Prefix Property
    H. J. Sander Bruggink · 2006 · Lecture notes in computer science
  66. A language for higher-order explanation-based learning
    Scott Dietzen · 1992 · Defense Technical Information Center (DTIC)
  67. Cut Elimination for a Logic with Generic Judgments and Induction
    Alwen Fernanto Tiu · 2008 · arXiv (Cornell University)
  68. Tractable and intractable second-order matching problems
    Kouichi Hirata, Keizo Yamada, Masateru Harao · 2003 · Journal of Symbolic Computation
  69. Term Sequent Logic
    Michael Gabbay, Murdoch J. Gabbay · 2009 · Electronic Notes in Theoretical Computer Science
  70. Anti-Unification Algorithms: Design, Analysis, and Implementation
    At Linz, Johannes Kepler · 2015
  71. Logical closures
    Dominic Duggan · 1994 · Lecture notes in computer science
  72. Generic automatic proof tools
    Lawrence Charles Paulson · 2021 · arXiv (Cornell University)
  73. Representing Communicative Intentions in Collaborative Conversational Agents
    Matthew Stone · 2001
  74. Now f is continuous (exercise!)
    R. D. Arthan · 2014 · DOAJ (DOAJ: Directory of Open Access Journals)
  75. Unification of Hypergraph $$\lambda $$-Terms
    Alimujiang Yasen, Kazunori Ueda · 2017 · Lecture notes in computer science
  76. A dependently typed calculus with polymorphic subtyping
    Mingqi Xue, Bruno C. d. S. Oliveira · 2021 · Science of Computer Programming
  77. Reasoning about Computations Using Two-Levels of Logic
    Dale Miller · 2010 · Lecture notes in computer science
  78. Identifying Polynomial-Time Recursive Functions
    Carsten Schürmann, Jatin Shah · 2005 · Lecture notes in computer science
  79. Constraint solving in non-permutative nominal abstract syntax
    Matthew R. Lakin · 2011 · Logical Methods in Computer Science
  80. Decidable Variants of Higher-Order Unification
    Manfred Schmidt-Schauß · 2005 · Lecture notes in computer science
  81. Nominal uni cation
    Christian Urban, Andrew M. Pitts, Murdoch J. Gabbay · 2004
  82. Rewriting Modulo β in the λΠ-Calculus Modulo
    Ronan Saillard · 2015 · Electronic Proceedings in Theoretical Computer Science
  83. Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding
    Makoto Hamana · 2022 · Mathematical Structures in Computer Science
  84. Reciprocal Influences Between Proof Theory and Logic Programming
    Dale Miller · 2019 · Philosophy & Technology
  85. Functional and Constraint Logic Programming
    2019 · Lecture notes in computer science
  86. Proof Search in Minimal Logic
    Helmut Schwichtenberg · 2004 · Lecture notes in computer science
  87. Descendants and Head Normalization of Higher-Order Rewrite Systems
    Hideto Kasuya, Masahiko Sakai, Kiyoshi Agusa · 2002 · Lecture notes in computer science
  88. Higher-order narrowing with convergent systems
    Christian Prehofer · 1995 · Lecture notes in computer science
  89. Implementing λ-calculus reduction strategies in extended logic programming languages
    John Hannan · 2005 · Springer eBooks
  90. The Relative Complement Problem for Higher-Order Patterns
    1999 · The MIT Press eBooks
  91. The Full Abstraction Problem for Higher Order Functional-Logic Programs
    Francisco J. López-Fraguas, Juan Rodríguez-Hortalá · 2010 · arXiv (Cornell University)
  92. Abstract deduction and inferential models for type theory
    Paolo Gentilini, Maurizio Martelli · 2010 · Information and Computation
  93. A modular semantics for higher-order declarative programming with constraints
    Rafael del Vado Vírseda, Fernando Pérez Morente · 2011
  94. The RTA List of Open Problems
    Nachum Dershowitz, Ralf Treinen · 2010
  95. Unification of Higher-order Patterns modulo Simple Syntactic Equational Theories
    Alexandre Boudet · 2000 · Discrete Mathematics & Theoretical Computer Science
  96. Permissive nominal terms
    Gilles Dowek B, Murdoch J. Gabbay, Dominic P. Mulligan · 2008 · HAL
  97. A bottom-up interpreter for a higher-order logic programming language
    Alain Hui Bon Hoa · 2006 · Springer eBooks
  98. A Higher-Order Abstract Syntax Approach to the Verified Compilation of Functional Programs
    Yuting Wang · 2017 · arXiv (Cornell University)
  99. Proof Search Specifications of Bisimulation and Modal Logics for the pi-Calculus
    Alwen Fernanto Tiu, Dale Miller · 2008 · arXiv (Cornell University)
  100. The New Rewriting Engine of Dedukti
    Gabriel Hondet, Frédéric Blanqui · 2020 · arXiv (Cornell University)