On the expressivity of minimal generic quantification

DOI10.1016/J.ENTCS.2008.12.113MaRDI QIDQ2804937zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

proof theoryfixed pointshigher-order abstract syntaxgeneric quantification

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Logic in computer science (03B70)

Recommendations

• A logic for reasoning about generic judgments
• Modelling generic judgements
• A proof theory for generic judgments
• scientific article; zbMATH DE number 2014706
• Computer Science Logic

Cites work

• scientific article; zbMATH DE number 1696799 (Why is no real title available?)
• A logic for reasoning about generic judgments
• A proof theory for generic judgments
• A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
• CONCUR 2005 – Concurrency Theory
• On the expressivity of minimal generic quantification
• Reasoning with higher-order abstract syntax in a logical framework
• The Abella Interactive Theorem Prover (System Description)
• Uniform proofs as a foundation for logic programming

Cited in

(10)

• scientific article; zbMATH DE number 1615238 (Why is no real title available?)
• On the generation of quantified lemmas
• Mechanized metatheory revisited
• Focused Inductive Theorem Proving
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• ASP and subset minimality: enumeration, cautious reasoning and MUSes
• Nominal abstraction
• On the expressibility hierarchy of Magidor-Malitz quantifiers
• Proof pearl: Abella formalization of \(\lambda \)-calculus cube property
• On the expressivity of minimal generic quantification

Describes a project that uses

Uses Software

• Abella
• Bedwyr
• Tac
• Twelf

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)