On the expressivity of minimal generic quantification
From MaRDI portal
Publication:2804937
DOI10.1016/J.ENTCS.2008.12.113zbMATH Open1337.03038OpenAlexW2017595664MaRDI QIDQ2804937FDOQ2804937
Authors: David Baelde 
Publication date: 6 May 2016
Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.entcs.2008.12.113
Recommendations
Proof theory in general (including proof-theoretic semantics) (03F03) Logic in computer science (03B70)
Cites Work
- The Abella Interactive Theorem Prover (System Description)
- On the expressivity of minimal generic quantification
- A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
- Reasoning with higher-order abstract syntax in a logical framework
- Uniform proofs as a foundation for logic programming
- Least and Greatest Fixed Points in Linear Logic
- Title not available (Why is that?)
- A proof theory for generic judgments
- CONCUR 2005 – Concurrency Theory
- A logic for reasoning about generic judgments
Cited In (10)
- Title not available (Why is that?)
- On the generation of quantified lemmas
- Mechanized metatheory revisited
- Focused Inductive Theorem Proving
- ASP and subset minimality: enumeration, cautious reasoning and MUSes
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
- Nominal abstraction
- Proof pearl: Abella formalization of \(\lambda \)-calculus cube property
- On the expressibility hierarchy of Magidor-Malitz quantifiers
- On the expressivity of minimal generic quantification
Uses Software
This page was built for publication: On the expressivity of minimal generic quantification
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2804937)
