I was a postdoctoral researcher at the Chair for Logic and Verification at the Technische Universität München until November 2017. I joined the group as a Ph.D. student in 2011 and defended my thesis in 2016. I obtained my master degree at the Charles University in Prague, Czech Republic.
My research focuses on holistic security of webbased systems, interactive theorem proving, developement of automation for type systems of HOLbased provers, and foundations of higherorder logic. As a postdoctoral researcher, I worked in the RS3 project.
email: kuncar@in.tum.de
Publications
Journals

From Types to Sets by Local Type Definitions in HigherOrder Logic
Ondřej Kunčar, Andrei Popescu. Journal of Automated Reasoning, 2018.
Web page  PDF 
A Consistent Foundation for Isabelle/HOL
Ondřej Kunčar, Andrei Popescu. Journal of Automated Reasoning, 2018.
Web page  PDF
Conferences
 Safety and Conservativity of Definitions in HOL and Isabelle/HOL.
Ondřej Kunčar, Andrei Popescu.
To appear at POPL2018. 
Distributed Verification of Smart Contracts
Chad E. Brown, Ondřej Kunčar, Josef Urban
abstract poster
Accepted to the poster session of ITP '17.  Comprehending Isabelle/HOL's Consistency.
Ondřej Kunčar, Andrei Popescu.
To appear at ESOP 2017.  From Types to Sets by Local Type Definitions in HigherOrder Logic.
Ondřej Kunčar, Andrei Popescu.
Proceedings of the ITP '16 (© Springer).  A Consistent Foundation for Isabelle/HOL.
Ondřej Kunčar, Andrei Popescu.
Proceedings of the ITP '15 (© Springer).  Correctness of Isabelle's Cyclicity Checker: Implementability of Overloading in Proof Assistants.
Ondřej Kunčar.
Proceedings of the CPP '15 (© ACM).  Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL.
Brian Hufmann, Ondřej Kunčar.
Proceedings of the CPP '13 (© Springer).  Data Refinement in Isabelle/HOL.
Florian Haftmann, Alexander Krauss, Ondřej Kunčar, Tobias Nipkow.
Proceedings of the ITP '13 (© Springer).  Proving Valid Quantiﬁed Boolean Formulas in HOL Light.
Ondřej Kunčar.
Proceedings of the ITP '11 (© Springer). BibTeX
 Reconstruction of the Mizar Type System in the HOL Light System.
Ondřej Kunčar.
Proceedings of the WDS'10. BibTeX
Workshops
 From Types to Sets in Isabelle/HOL.
Ondřej Kunčar, Andrei Popescu.
Isabelle Workshop 2014.
 Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL.
Brian Huffman, Ondřej Kunčar.
Isabelle Users Workshop 2012.
Ph.D. thesis

Types, Abstraction and Parametric Polymorphism in HigherOrder Logic.
Ondřej Kunčar. Ph.D. thesis.
Fakultät für Informatik, Technische Universität München, April 2016.
Master thesis

Systems For Formal Mathematics [only Czech].
Ondřej Kunčar. Master thesis.
Faculty of Mathematics and Physics, Charles University, Prague. September 2009.