An improved implementation and abstract interface for Hybrid

DOI10.4204/EPTCS.71.6MaRDI QIDQ6940441zbMATH OpenFDO

Authors Alan J. Martin, Amy P. Felty

Publication date 19 August 2025

Copyright license Creative Commons license

Full work available at URL https://doi.org/10.4204/EPTCS.71.6

Mathematics Subject Classification ID

Formalization of mathematics in connection with theorem provers (68V20)

Cites work

• A hybrid encoding of Howe's method for establishing congruence of bisimilarity
• A new approach to abstract syntax with variable binding
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
• Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq
• Higher-order abstract syntax in type theory
• scientific article; zbMATH DE number 2185657 (Why is no real title available?)
• scientific article; zbMATH DE number 1927412 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• Isabelle/HOL. A proof assistant for higher-order logic
• Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations
• Nominal logic, a first order theory of names and binding
• Nominal techniques in Isabelle/HOL
• Reasoning with higher-order abstract syntax and contexts: a comparison
• The Abella Interactive Theorem Prover (System Description)
• Two-level hybrid: a system for reasoning using higher-order abstract syntax

This page was built for publication: An improved implementation and abstract interface for Hybrid

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