Programming with Higher-Order Logic

DOI10.1017/CBO9781139021326zbMath1267.68014OpenAlexW4206717895MaRDI QIDQ2891520

Gopalan Nadathur, Dale A. Miller

Publication date: 15 June 2012

Full work available at URL: https://doi.org/10.1017/cbo9781139021326

zbMATH Keywords

higher-order logiclambda calculusProloghigher-order unification

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (35)

The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey ⋮ Functions-as-constructors higher-order unification: extended pattern unification ⋮ The undecidability of proof search when equality is a logical connective ⋮ Proof checking and logic programming ⋮ The Lean Theorem Prover (System Description) ⋮ The Proof Certifier Checkers ⋮ Extracting Proofs from Tabled Proof Search ⋮ Fifty Years of Prolog and Beyond ⋮ A Survey of the Proof-Theoretic Foundations of Logic Programming ⋮ In Praise of Impredicativity: A Contribution to the Formalization of Meta-Programming ⋮ Lang-n-Send Extended: Sending Regular Expressions to Monitors ⋮ Unnamed Item ⋮ A semantic framework for proof evidence ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them ⋮ Proof certificates for equality reasoning ⋮ Equivalence of two fixed-point semantics for definitional higher-order logic programs ⋮ Proof Checking and Logic Programming ⋮ PNL to HOL: from the logic of nominal sets to the logic of higher-order functions ⋮ A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs ⋮ 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 ⋮ Extensional Semantics for Higher-Order Logic Programs with Negation ⋮ 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 ⋮ Encoding Generic Judgments ⋮ Formalization of metatheory of the Quipper quantum programming language in a linear logic ⋮ Unnamed Item ⋮ From the universality of mathematical truth to the interoperability of proof systems

Uses Software

• Haskell

This page was built for publication: Programming with Higher-Order Logic