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

Benzmüller, ChristophChristophBenzmüller0000-0002-3392-3093Kirchner, DanielDanielKirchner0000-0001-9229-11482026-09-102026-09-1020262150-914xhttps://fis.uni-bamberg.de/handle/uniba/117133engMonadic Second-Order Logic in HOL : Deep and Shallow Embeddings with Automated Faithfulness (Isabelle/HOL dataset)articlehttps://isa-afp.org/entries/MSOinHOL.html