Pages that link to "Item:Q2891520"
From MaRDI portal
The following pages link to Programming with Higher-Order Logic (Q2891520):
Displaying 35 items.
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey (Q287277) (← links)
- Equivalence of two fixed-point semantics for definitional higher-order logic programs (Q512650) (← links)
- PNL to HOL: from the logic of nominal sets to the logic of higher-order functions (Q714797) (← links)
- A semantic framework for proof evidence (Q1701039) (← links)
- Proof certificates for equality reasoning (Q1744408) (← links)
- On the effectiveness of higher-order logic programming in language-oriented programming (Q2039939) (← links)
- System description: lang-n-change -- a tool for transforming languages (Q2039949) (← links)
- The Lean 4 theorem prover and programming language (Q2055901) (← links)
- From the universality of mathematical truth to the interoperability of proof systems (Q2104491) (← links)
- Functions-as-constructors higher-order unification: extended pattern unification (Q2134936) (← links)
- The undecidability of proof search when equality is a logical connective (Q2134939) (← links)
- Formalization of metatheory of the Quipper quantum programming language in a linear logic (Q2331074) (← links)
- Proof checking and logic programming (Q2628296) (← links)
- A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs (Q2802499) (← links)
- Extensional Semantics for Higher-Order Logic Programs with Negation (Q2835890) (← links)
- Encoding Generic Judgments (Q2841234) (← links)
- Extracting Proofs from Tabled Proof Search (Q2938048) (← links)
- (Q3384904) (← links)
- The Lean Theorem Prover (System Description) (Q3454108) (← links)
- The Proof Certifier Checkers (Q3455771) (← links)
- (Q5014440) (← links)
- (Q5015283) (← links)
- (Q5028439) (← links)
- In Praise of Impredicativity: A Contribution to the Formalization of Meta-Programming (Q5108530) (← links)
- The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them (Q5140030) (← links)
- (Q5155663) (← links)
- Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search (Q5236550) (← links)
- Implementing type theory in higher order constraint logic programming (Q5236551) (← links)
- A case study in programming coinductive proofs: Howe’s method (Q5236557) (← links)
- A general proof certification framework for modal logic (Q5236558) (← links)
- Proof Checking and Logic Programming (Q5743582) (← links)
- (Q5875441) (← links)
- Fifty Years of Prolog and Beyond (Q6063890) (← links)
- A Survey of the Proof-Theoretic Foundations of Logic Programming (Q6063891) (← links)
- Lang-n-Send Extended: Sending Regular Expressions to Monitors (Q6122642) (← links)