Daniel Kirchner

A deep embedding of HOL in HOL: soundness, completeness, consistency

by Christoph Benzmüller and Daniel Kirchner

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

by Christoph Benzmüller and Daniel Kirchner

Abstract Object Theory

by Daniel Kirchner

Representation and Partial Automation of the Principia Logico-Metaphysica in Isabelle/HOL

by Daniel Kirchner