Monadic Second-Order Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness (Isabelle/HOL dataset)

Christoph Benzmüller, Daniel Kirchner. Monadic Second-Order Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness (Isabelle/HOL dataset). Archive of Formal Proofs, 2026, 2026. [doi]

Abstract

Abstract is missing.