Two applications of logic programming to Coq
From MaRDI portal
Cites work
- -calculus in (Co)inductive-type theory
- A Linear Spine Calculus
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- A multi-focused proof system isomorphic to expansion proofs
- A semantic framework for proof evidence
- A Sequent Calculus for Type Theory
- A two-level logic approach to reasoning about computations
- Abella: a system for reasoning about relational specifications
- Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
- Edinburgh LCF. A mechanized logic of computation
- Efficient generation of test data structures using constraint logic programming and program transformation
- ELPI: fast, embeddable, Prolog interpreter
- Focusing and polarization in linear, intuitionistic, and classical logics
- Foundational property-based testing
- Full intuitionistic linear logic
- Hierarchy builder: algebraic hierarchies made easy in Coq with Elpi (system description)
- Higher-order Horn clauses
- scientific article; zbMATH DE number 1701361 (Why is no real title available?)
- scientific article; zbMATH DE number 2185657 (Why is no real title available?)
- scientific article; zbMATH DE number 4035108 (Why is no real title available?)
- scientific article; zbMATH DE number 4053062 (Why is no real title available?)
- scientific article; zbMATH DE number 42752 (Why is no real title available?)
- scientific article; zbMATH DE number 2079018 (Why is no real title available?)
- scientific article; zbMATH DE number 7649978 (Why is no real title available?)
- Implementing tactics and tacticals in a higher-order logic programming language
- Implementing type theory in higher order constraint logic programming
- Least and greatest fixed points in linear logic
- Linear logic
- Logic Programming with Focusing Proofs in Linear Logic
- Mechanized metatheory revisited
- Multi-focused proofs with different polarity assignments
- Parametric higher-order abstract syntax for mechanized semantics
- Partial evaluation in logic programming
- Programming with higher-order logic.
- Proof checking and logic programming
- Strongly typed term representations in Coq
- Tests and proofs. 10th international conference, TAP 2016, held as part of STAF 2016, Vienna, Austria, July 5--7, 2016. Proceedings
- The \textsc{MetaCoq} project
- The foundation of a generic theorem prover
- The ILTP problem library for intuitionistic logic
- Translating between implicit and explicit versions of proof
- Uniform proofs as a foundation for logic programming
- Untersuchungen über das logische Schließen. I.
- αCheck: A mechanized metatheory model checker
This page was built for publication: Two applications of logic programming to Coq
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7232188)
