Ondrej Kuncar

According to our database, Ondrej Kuncar authored at least 13 papers between 2011 and 2019.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2019

A Consistent Foundation for Isabelle/HOL.

Ondrej Kuncar, Andrei Popescu

J. Autom. Reason., 2019

From Types to Sets by Local Type Definition in Higher-Order Logic.

Ondrej Kuncar, Andrei Popescu

J. Autom. Reason., 2019

2018

Safety and conservativity of definitions in HOL and Isabelle/HOL.

Ondrej Kuncar, Andrei Popescu

Proc. ACM Program. Lang., 2018

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

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

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, Christian Sternagel, René Thiemann, Dmitriy Traytel

Proceedings of the Frontiers of Combining Systems - 11th International Symposium, 2017

Comprehending Isabelle/HOL's Consistency.

Ondrej Kuncar, Andrei Popescu

Proceedings of the Programming Languages and Systems, 2017

2016

Types, Abstraction and Parametric Polymorphism in Higher-Order Logic.

Ondrej Kuncar

PhD thesis, 2016

Perron-Frobenius Theorem for Spectral Radius Analysis.

Jose Divasón, Ondrej Kuncar, René Thiemann, Akihisa Yamada

Arch. Formal Proofs, 2016

From Types to Sets by Local Type Definitions in Higher-Order Logic.

Ondrej Kuncar, Andrei Popescu

Proceedings of the Interactive Theorem Proving - 7th International Conference, 2016

2015

Correctness of Isabelle's Cyclicity Checker: Implementability of Overloading in Proof Assistants.

Ondrej Kuncar

Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015

2013

Data Refinement in Isabelle/HOL.

Florian Haftmann, Alexander Krauss, Ondrej Kuncar, Tobias Nipkow

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL.

Brian Huffman, Ondrej Kuncar

Proceedings of the Certified Programs and Proofs - Third International Conference, 2013

2011

Proving Valid Quantified Boolean Formulas in HOL Light.

Ondrej Kuncar

Proceedings of the Interactive Theorem Proving - Second International Conference, 2011