Proving Valid Quantified Boolean Formulas in HOL Light. - Ondrej Kuncar (ITP, 2011)

Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL. - Brian Huffman; Ondrej Kuncar (CPP, 2013)

Data Refinement in Isabelle/HOL. - Florian Haftmann; Alexander Krauss 001; Ondrej Kuncar; Tobias Nipkow (ITP, 2013)

Correctness of Isabelle's Cyclicity Checker: Implementability of Overloading in Proof Assistants. - Ondrej Kuncar (CPP, 2015)

From Types to Sets by Local Type Definitions in Higher-Order Logic. - Ondrej Kuncar; Andrei Popescu 001 (ITP, 2016)

Perron-Frobenius Theorem for Spectral Radius Analysis. - Jose Divasón; Ondrej Kuncar; René Thiemann; Akihisa Yamada 002 (Arch. Formal Proofs, 2016)

Types, Abstraction and Parametric Polymorphism in Higher-Order Logic. - Ondrej Kuncar (2016)

Comprehending Isabelle/HOL's Consistency. - Ondrej Kuncar; Andrei Popescu 001 (ESOP, 2017)

Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. - Julian Biendarra; Jasmin Christian Blanchette; Aymeric Bouzy; Martin Desharnais; Mathias Fleury; Johannes Hölzl; Ondrej Kuncar; Andreas Lochbihler; Fabian Meier; Lorenz Panny; Andrei Popescu 001; Christian Sternagel; et al. (FroCoS, 2017)

Efficient certification of complexity proofs: formalizing the Perron-Frobenius theorem (invited talk paper). - Jose Divasón; Sebastiaan J. C. Joosten; Ondrej Kuncar; René Thiemann; Akihisa Yamada 002 (CPP, 2018)

Safety and conservativity of definitions in HOL and Isabelle/HOL. - Ondrej Kuncar; Andrei Popescu 001 (Proc. ACM Program. Lang., 2018)

From Types to Sets by Local Type Definition in Higher-Order Logic. - Ondrej Kuncar; Andrei Popescu 001 (J. Autom. Reason., 2019)

A Consistent Foundation for Isabelle/HOL. - Ondrej Kuncar; Andrei Popescu 001 (J. Autom. Reason., 2019)