Programming with higher-order logic.
From MaRDI portal
Logic in computer science (03B70) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Theory of programming languages (68N15) Logic programming (68N17) Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)
Cited in
(57)- Adapting functional programs to higher order logic
- Implementing tactics and tacticals in a higher-order logic programming language
- A semantic framework for proof evidence
- Proof certificates for equality reasoning
- On the effectiveness of higher-order logic programming in language-oriented programming
- System description: lang-n-change -- a tool for transforming languages
- The Lean 4 theorem prover and programming language
- From the universality of mathematical truth to the interoperability of proof systems
- Functions-as-constructors higher-order unification: extended pattern unification
- The undecidability of proof search when equality is a logical connective
- Formalization of metatheory of the Quipper quantum programming language in a linear logic
- Proof checking and logic programming
- scientific article; zbMATH DE number 1692888 (Why is no real title available?)
- A higher-order abstract syntax approach to verified transformations on functional programs
- Encoding generic judgments: preliminary results
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
- Higher-order logic learning and Progol
- Extracting proofs from tabled proof search
- On the use of advanced logic programming languages in computational linguistics
- Towards coinductive theory exploration in Horn clause logic: position paper
- The Lean theorem prover (system description)
- The Proof Certifier Checkers
- scientific article; zbMATH DE number 4053062 (Why is no real title available?)
- scientific article; zbMATH DE number 1926604 (Why is no real title available?)
- scientific article; zbMATH DE number 3992920 (Why is no real title available?)
- scientific article; zbMATH DE number 3999279 (Why is no real title available?)
- scientific article; zbMATH DE number 2090550 (Why is no real title available?)
- Equivalence of two fixed-point semantics for definitional higher-order logic programs
- Certification of prefixed tableau proofs for modal logic
- Efficient full higher-order unification
- A logic programming language with lambda-abstraction, function variables, and simple unification
- In praise of impredicativity: a contribution to the formalization of meta-programming
- Equivalence of two fixed-point semantics for definitional higher-order logic programs
- The new normal: we cannot eliminate cuts in coinductive calculi, but we can explore them
- A characterisation of open bisimilarity using an intuitionistic modal logic
- Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search
- Implementing type theory in higher order constraint logic programming
- A case study in programming coinductive proofs: Howe's method
- A general proof certification framework for modal logic
- Advances in Computer Science - ASIAN 2004. Higher-Level Decision Making
- Proof checking and logic programming
- scientific article; zbMATH DE number 7649978 (Why is no real title available?)
- Fifty Years of Prolog and Beyond
- A Survey of the Proof-Theoretic Foundations of Logic Programming
- Lang-n-Send Extended: Sending Regular Expressions to Monitors
- Reductive logic, proof-search, and coalgebra: a perspective from resource semantics
- From program logics towards language logics
- Hierarchy builder: algebraic hierarchies made easy in Coq with Elpi (system description)
- Efficient full higher-order unification
- Mechanized metatheory revisited: an extended abstract (invited paper)
- Equational reasoning modulo commutativity in languages with binders
- Object-level reasoning with logics encoded in HOL Light
- Logic program proportions
- Integrating logic rules with everything else, seamlessly
- PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
- Two applications of logic programming to Coq
- Barendregt's theory of the -calculus, refreshed and formalized
This page was built for publication: Programming with higher-order logic.
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2891520)
