scientific article; zbMATH DE number 1927412

MaRDI QIDQ4484329zbMATH OpenFDO

Authors Simon J. Ambler, Roy L. Crole, Alberto Momigliano

Publication date 12 June 2003

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2410/24100013.htm

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• Two-level hybrid: a system for reasoning using higher-order abstract syntax
• scientific article; zbMATH DE number 1956525
• Reasoning with higher-order abstract syntax in a logical framework
• Higher-order abstract syntax in type theory

Cited in

(13)

• A focused linear logical framework and its application to metatheory of object logics
• Formalization of metatheory of the Quipper quantum programming language in a linear logic
• Formal meta-level analysis framework for quantum programming languages
• Canonical HybridLF: extending Hybrid with dependent types
• Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations
• scientific article; zbMATH DE number 1956525 (Why is no real title available?)
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• The representational adequacy of Hybrid
• Higher-order abstract syntax in type theory
• scientific article; zbMATH DE number 1670748 (Why is no real title available?)
• Nominal techniques in Isabelle/HOL
• A hybrid encoding of Howe's method for establishing congruence of bisimilarity
• Two-level hybrid: a system for reasoning using higher-order abstract syntax

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4484329)