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 301–380 of 380

  1. A Framework for Reasoning About LF Specifications
    Mary Southern · 2021 · arXiv (Cornell University)
  2. The Semantics of Nominal Logic Programs
    James Cheney · 2006 · Lecture notes in computer science
  3. Dependently-Typed Termination and Embedding of Extensional Universe-Polymorphic Type Theory using Rewriting
    Guillaume Genestier · 2020
  4. The undecidability of proof search when equality is a logical connective
    Dale Miller, Alexandre Viel · 2021 · Annals of Mathematics and Artificial Intelligence
  5. The 2006 Federated Logic Conference
    Towers Seattle · 2006
  6. Trace matching in a concurrent logical framework
    Iliano Cervesato A, Frank Pfenning, Jorge Luis Sacchini, Carsten Schürmann, Robert J. Simmons · 2012 · International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP)
  7. Lightweight Higher-Order Rewriting in Haskell
    Emil Axelsson, Andrea Vezzosi · 2016 · Lecture notes in computer science
  8. Functional programming with λ-tree syntax
    Ulysse Gérard, Dale Miller, Gabriel Scherer · 2019 · International Symposium on Principles and Practice of Declarative Programming (PPDP)
  9. A Logical Framework with Higher-Order Rational (Circular) Terms
    Zhibo Chen, Frank Pfenning · 2023 · Lecture notes in computer science
  10. Equational Reasoning Modulo Commutativity in Languages with Binders
    Ali K. Caires-Santos, Maribel Fernández, Daniele Nantes-Sobrinho · 2025 · Lecture notes in computer science
  11. The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting
    Johannes Niederhauser, Aart Middeldorp · 2025 · Lecture notes in computer science
  12. Checking foundational proof certificates for first-order logic
    Zakaria Chihani, Dale Miller, Fabien Renaud · 2013
  13. Schematic Polymorphism in the Abella Proof Assistant
    Gopalan Nadathur, Yuting Wang · 2018 · International Symposium on Principles and Practice of Declarative Programming (PPDP)
  14. Modular Termination for Second-Order Computation Rules and Application to Algebraic Effect Handlers
    Makoto Hamana · 2022 · Logical Methods in Computer Science
  15. Semantics of a Relational $$\lambda $$-Calculus
    Pablo Barenbaum, Federico Lochbaum, Mariana Milicich · 2020 · Lecture notes in computer science
  16. Confluence of Terminating Rewriting Computations
    Jean-Pierre Jouannaud · 2023 · Springer eBooks
  17. Structures et modèles de calculs de réécriture
    Germain Faure · 2007 · Publications Et Travaux Academiques de Lorraine (Universite de Lorraine)
  18. Cooperation of Algebraic Constraint Domains in Higher-Order Functional and Logic Programming
    Rafael del Vado Vírseda · 2011 · Lecture notes in computer science
  19. Free variables and subexpressions in higher-order meta logic
    Chuck C. Liang · 1998 · Lecture notes in computer science
  20. Reduction Strategies in Lambda Term Normalization and their Effects on Heap Usage
    Xiaochu Qi · 2004 · arXiv (Cornell University)
  21. Ramified higher-order unification
    Jean Goubault-Larrecq · 2002 · ACM/IEEE Symposium on Logic in Computer Science (LICS)
  22. Untyped Constrained Lambda Calculus
    John Newsome Crossley, Luis Mandel, Martin Wirsing · 1993
  23. A Theoretical Framework for the Higher-Order Cooperation of Numeric Constraint Domains
    Rafael del Vado Vírseda · 2011 · Electronic Notes in Theoretical Computer Science
  24. Recognizability of Redexes for Higher-Order Rewrite Systems
    Hideto Kasuya, Masahiko Sakai, Kiyoshi Agusa · 2009 · IPSJ Online Transactions
  25. Higher-Order Substitutions
    Dominic Duggan · 2001 · Information and Computation
  26. CLP(H): Constraint Logic Programming for Hedges
    Besik Dundua, Mário Florido, Temur Kutsia, Mircea Marin · 2015 · arXiv (Cornell University)
  27. Using higher-order logic programming for semantic interpretation of coordinate constructs
    Seth Kulick A · 1995 · Proceedings of the conference - Association for Computational Linguistics. Meeting
  28. Higher-order dependency pairs
    Frédéric Blanqui · 2018 · arXiv (Cornell University)
  29. PlinyCompute: A Platform for High-Performance, Distributed, Data-Intensive Tool Development
    Jia Zou, Barnett, R. Matthew, Tania Lorido-Botrán, Shangyu Luo, Carlos Rodríguez Monroy, Sourav Sikdar, Kia Teymourian, Binhang Yuan, Chris Jermaine · 2017 · arXiv (Cornell University)
  30. Superposition with Lambdas
    Alexander Bentkamp, Jasmin Christian Blanchette, Sophie Tourret, Petar Vukmirović, Uwe Waldmann · 2021 · arXiv (Cornell University)
  31. Extensions of nominal terms
    Dominic P. Mulligan · 2011
  32. Samsara
    John Newsome Crossley · 2006 · Springer eBooks
  33. Refinements of lazy narrowing for left-linear fully-extended pattern rewrite systems
    Mircea Marin, Taro Suzuki, 哲雄 井田, 筑波大学電子・情報工学系 · 2001
  34. Applications of Foundational Proof Certificates in theorem proving
    Roberto Blanco Martínez · 2017
  35. Introduction to the Literature on Programming Language Design
    Gary Todd Leavens · 1996 · Iowa State University Digital Repository (Iowa State University)
  36. Implementing higher-order functions in an algebraic specification language with narrowing
    Bernhard Reus · 2006 · Springer eBooks
  37. Logic Programming and Meta-Logic
    Dale Miller · 1997 · Springer eBooks
  38. Program analysis in λprolog
    John Hannan · 1998 · Lecture notes in computer science
  39. Coherence for cartesian closed categories: A sequential approach
    Akira S. Mori, Yoshihiro Matsumoto · 1995 · Lecture notes in computer science
  40. Existential type systems between Church and Curry style (type-free style)
    Ken-etsu Fujita, Aleksy Schubert · 2014 · Theoretical Computer Science
  41. Contextual equivalence for inductive definitions with binders in higher order typed functional programming
    Matthew R. Lakin, Andrew M. Pitts · 2013 · Journal of Functional Programming
  42. Application of Metaprogramming to Program Generation
    Emir Pasalic, Tim Sheard, Walid Taha · 2000
  43. Head-Needed Strategy of Higher-Order Rewrite Systems and Its Decidable Classes
    Hideto Kasuya, Masahiko Sakai, Kiyoshi Agusa · 2009 · IPSJ Online Transactions
  44. The Logic of Sense and Reference
    Reinhard Muskens · 2009
  45. Intuitionistic resolution for a logic programming language with scoping constructs
    Alain Hui Bon Hoa · 1994 · Lecture notes in computer science
  46. Logic Programming and Type Inference with the Calculus of Constructions
    Matthew Mirman · 2014
  47. HybridLF : a system for reasoning in higher-order abstract syntax
    Amy Elizabeth Furniss · 2015 · Leicester Research Archive (University of Leicester)
  48. A-sufficient substitutions in mixed contexts
    Per Kreuger · 1994
  49. Programming with Proofs and Explicit Contexts (Extended Abstract)
    Brigitte Pientka, Joshua Dunfield · 2008
  50. On the Limits of Second-Order Unification
    Jordi Levy · 2014 · DIGITAL.CSIC (Spanish National Research Council (CSIC))
  51. Constraint handling rules with binders, patterns and generic quantification
    Alejandro Serrano, Jurriaan Hage · 2017 · Theory and Practice of Logic Programming
  52. Higher-Order Equational Pattern Anti-Unification [Preprint]
    David M. Cerna, Temur Kutsia · 2018 · arXiv (Cornell University)
  53. A Simple Semi-automated Proof Assistant for First-order Modal Logics.
    Tomer Libal · 2018
  54. Automatic Termination Analysis Using WANDA
    Cynthia Kop · 2018 · Radboud Repository (Radboud University)
  55. Uniform Provability in Classical Logic
    Gopalan Nadathur · 1998 · arXiv (Cornell University)
  56. Correspondences between Classical, Intuitionistic and Uniform Provability
    Gopalan Nadathur · 1998 · arXiv (Cornell University)
  57. A static higher-order dependency pair framework
    Carsten Fuhs, Cynthia Kop · 2019 · BIROn (Birkbeck, University of London)
  58. From LCF to Isabelle/HOL
    Lawrence Charles Paulson, Tobias Nipkow, Makarius Wenzel · 2019 · Formal Aspects of Computing
  59. Kanren Light: A Dynamically Semi-Certified Interactive Logic Programming System
    Marco Maggesi, Nocentini, Massimo · 2020 · arXiv (Cornell University)
  60. Semantics of a Relational λ-Calculus (Extended Version)
    Pablo Barenbaum, Federico Lochbaum, Mariana Milicich · 2020 · arXiv (Cornell University)
  61. References
    Arno Scharl A · 2000 · Applied computing
  62. Hobbits for Haskell
    Edwin Westbrook, Nicolas Frisby, Paul Brauner · 2011 · ACM SIGPLAN Notices
  63. Intensional logic
    Paul Gochet · 2010 · John Benjamins Publishing Company eBooks
  64. Intensional logic
    Paul Gochet · 2022 · Handbook of pragmatics online/Handbook of pragmatics
  65. Foundations of Haskell’s Rewrite Rules Based on Higher-Kinded Polymorphic Rewrite Systems
    Makoto Hamana · 2024 · Lecture notes in computer science
  66. A Saturation-Based Unification Algorithm for Higher-Order Rational Patterns
    Zhibo Chen, Frank Pfenning · 2024 · ACM Transactions on Computational Logic
  67. Generic Bidirectional Typing for Dependent Type Theories
    Thiago Felicissimo · 2025 · ACM Transactions on Programming Languages and Systems
  68. Hiord $^{{\kern2pt}\sharp}$ : An Approach to the Specification and Verification of Higher-Order (C)LP Programs
    MARCO CICCALÈ, DANIEL JURJO-RIVAS, José F. Morales, Pedro López-García, Manuel V. Hermenegildo · 2025 · Theory and Practice of Logic Programming
  69. Higher-Order Pattern Unification Modulo Similarity Relations
    Besik Dundua, Temur Kutsia · 2025 · Lecture notes in computer science
  70. Nominal anti-unification modulo equational theories
    Alexander Baumgartner, Daniele Nantes-Sobrinho · 2025 · Journal of Logical and Algebraic Methods in Programming
  71. Computing with relations, functions, and bindings
    Ulysse Gérard · 2019
  72. Higher-Order Confluence and Universe Embedding in the Logical Framework
    Gaspard Férey · 2021
  73. Integrating Automated Theorem Provers in Proof Assistants
    Yacine El Haddad · 2021
  74. Expressing predicate subtyping in computational logical frameworks
    Gabriel Hondet · 2022
  75. Generic bidirectional typing in a logical framework for dependent type theories
    Thiago Felicissimo · 2024
  76. ReCheck: Automated Contextual Improvement Verifier for Functional Calculi across User-Defined Operational Semantics
    Makoto Hamana, Kento Emoto · 2026 · Lecture notes in computer science
  77. Semantics of pattern unification
    Ambroise Lafont, Neel Krishnaswami · 2026 · Journal of Functional Programming
  78. Typed term evaluation systems with refinements for contextual improvement
    Koko Muroya, Makoto Hamana · 2026 · Science of Computer Programming
  79. Automating Proof Search when Equality is a Logical Connective
    Kaustuv Chaudhuri, Arunava Gantait, Dale Miller · 2026 · Lecture notes in computer science
  80. Imagining CLP(Λ,≡αβ)
    Olivier Ridoux · 1995 · Lecture notes in computer science