A new foundation for Nominal Isabelle

DOI10.1007/978-3-642-14052-5_5zbMATH Open1291.68350OpenAlexW1544467561MaRDI QIDQ5747640FDOQ5747640

Authors: Brian Huffman, Christian Urban 

Publication date: 14 September 2010

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-14052-5_5

Recommendations

• General bindings and alpha-equivalence in Nominal Isabelle
• General bindings and alpha-equivalence in Nominal Isabelle
• Nominal techniques in Isabelle/HOL
• Automated Deduction – CADE-20
• Reasoning about constants in Nominal Isabelle or how to formalize the second fixed point theorem

Mathematics Subject Classification ID

Cited In (10)

• Generic Authenticated Data Structures, Formally.
• Automated Deduction – CADE-20
• General bindings and alpha-equivalence in Nominal Isabelle
• HOCore in Coq
• General bindings and alpha-equivalence in Nominal Isabelle
• Psi-calculi in Isabelle
• Nominal techniques in Isabelle/HOL
• A consistent foundation for Isabelle/HOL
• Reasoning about constants in Nominal Isabelle or how to formalize the second fixed point theorem
• A consistent foundation for Isabelle/HOL

Uses Software

• Isabelle
• Isabelle/HOL
• Nominal Isabelle

This page was built for publication: A new foundation for Nominal Isabelle

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