The representational adequacy of <scp>Hybrid</scp>

DOI10.1017/S0960129511000041zbMath1248.68448OpenAlexW2013542353MaRDI QIDQ3008233

Roy L. Crole

Publication date: 15 June 2011

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129511000041

zbMATH Keywords

theorem provingIsabelle/HOLHybrid\(\lambda \)-expressionsde Bruijn expressionhigher-order abstract syntax (HOAS)

Mathematics Subject Classification ID

Related Items

Formalizing adequacy: a case study for higher-order abstract syntax, Alpha equivalence equalities, Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax, Canonical HybridLF: extending Hybrid with dependent types, Formalization of metatheory of the Quipper quantum programming language in a linear logic, Formal meta-level analysis framework for quantum programming languages, A focused linear logical framework and its application to metatheory of object logics

Uses Software

• ML
• Isabelle/HOL
• FreshOCaml

Cites Work

• Unnamed Item
• \(\pi\)-calculus in (Co)inductive-type theory
• A framework for defining logics