Ondřej Kunčar

Chair for Logic and Verification

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 web-based systems, interactive theorem proving, developement of automation for type systems of HOL-based provers, and foundations of higher-order logic. As a postdoctoral researcher, I worked in the RS3 project.

e-mail: kuncar@in.tum.de

Publications

Journals

• From Types to Sets by Local Type Definitions in Higher-Order 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 Higher-Order 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 Quantified 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 Higher-Order 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.