On the Expressivity of Minimal Generic Quantification

DOI10.1016/j.entcs.2008.12.113zbMath1337.03038OpenAlexW2017595664MaRDI QIDQ2804937

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

fixed pointsproof theoryhigher-order abstract syntaxgeneric quantification

Mathematics Subject Classification ID

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

Related Items (6)

The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey ⋮ Nominal abstraction ⋮ Proof Pearl: Abella Formalization of λ-Calculus Cube Property ⋮ Focused Inductive Theorem Proving ⋮ On the Expressivity of Minimal Generic Quantification ⋮ Mechanized metatheory revisited

Uses Software

• Twelf
• Tac
• Bedwyr
• Abella

Cites Work

• Uniform proofs as a foundation for logic programming
• On the Expressivity of Minimal Generic Quantification
• A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
• The Abella Interactive Theorem Prover (System Description)
• A proof theory for generic judgments
• Reasoning with higher-order abstract syntax in a logical framework
• Least and Greatest Fixed Points in Linear Logic
• CONCUR 2005 – Concurrency Theory
• Unnamed Item
• Unnamed Item

This page was built for publication: On the Expressivity of Minimal Generic Quantification