Canonical HybridLF: extending Hybrid with dependent types

DOI10.1016/j.entcs.2016.06.009zbMath1394.68351OpenAlexW2472567659WikidataQ113317680 ScholiaQ113317680MaRDI QIDQ1744412

Amy Furniss, Roy L. Crole

Publication date: 23 April 2018

Full work available at URL: https://doi.org/10.1016/j.entcs.2016.06.009

zbMATH Keywords

dependent typeslogical frameworksvariable bindingHOASmetalogical reasoning

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Uses Software

• HYBRID
• Isabelle
• Twelf

Cites Work

• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• The representational adequacy of <scp>Hybrid</scp>
• A framework for defining logics
• Parametric higher-order abstract syntax for mechanized semantics
• Mechanizing metatheory in a logical framework
• Types for Proofs and Programs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item