Programming with Higher-Order Logic
From MaRDI portal
Publication:2891520
DOI10.1017/CBO9781139021326zbMath1267.68014MaRDI QIDQ2891520
Gopalan Nadathur, Dale A. Miller
Publication date: 15 June 2012
Full work available at URL: https://doi.org/10.1017/cbo9781139021326
68N15: Theory of programming languages
68N18: Functional programming and lambda calculus
03B70: Logic in computer science
68Q55: Semantics in the theory of computing
68Q60: Specification and verification (program logics, model checking, etc.)
68-02: Research exposition (monographs, survey articles) pertaining to computer science
68N17: Logic programming
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Related Items
Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, In Praise of Impredicativity: A Contribution to the Formalization of Meta-Programming, The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them, 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, Unnamed Item, Proof Checking and Logic Programming, 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, The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey, Equivalence of two fixed-point semantics for definitional higher-order logic programs, PNL to HOL: from the logic of nominal sets to the logic of higher-order functions, 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, A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs, Extensional Semantics for Higher-Order Logic Programs with Negation, Encoding Generic Judgments, Extracting Proofs from Tabled Proof Search, Unnamed Item, The Lean Theorem Prover (System Description), The Proof Certifier Checkers
Uses Software
