Reducing higher-order recursion scheme equivalence to coinductive higher-order constrained Horn clauses
From MaRDI portal
Publication:6647302
DOI10.4204/EPTCS.344.4MaRDI QIDQ6647302
Publication date: 3 December 2024
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Krivine machines and higher-order schemes
- Semantics of infinite tree logic programming
- A representation of trees by languages. I
- Expressiveness of full first-order constraints in the algebra of finite or infinite trees
- \(L(A)=L(B)\)? decidability results from complete formal systems
- \(L(A)=L(B)\)? A simplified decidability proof.
- On the \(\lambda Y\) calculus
- Higher-order program verification via HFL model checking
- Horn Clause Solvers for Program Verification
- Böhm trees as higher-order recursion schemes
- Decidability of DPDA Language Equivalence via First-Order Grammars
- Theory of finite or infinite trees revisited
- Coinductive Logic Programming and Its Applications
- Productive corecursion in logic programming
- Higher-Order Model Checking: An Overview
- CONCUR 2004 - Concurrency Theory
- On the relationship between higher-order recursion schemes and higher-order fixpoint logic
- Co-Logic Programming: Extending Logic Programming with Coinduction
- Coalgebraic logic programming: from Semantics to Implementation
- Decidability of DPDA equivalence
- Coinduction in uniform: foundations for corecursive proof search with Horn clauses
This page was built for publication: Reducing higher-order recursion scheme equivalence to coinductive higher-order constrained Horn clauses
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6647302)
