Ondrej Kuncar

14 papers A 1B 7Journal 4Unranked 1
YearRankTypeTitle / Venue / Authors
2019 J jnl
A Consistent Foundation for Isabelle/HOL.
J. Autom. Reason.
Ondrej Kuncar, Andrei Popescu
2019 J jnl
From Types to Sets by Local Type Definition in Higher-Order Logic.
J. Autom. Reason.
Ondrej Kuncar, Andrei Popescu
2018 B conf
Efficient certification of complexity proofs: formalizing the Perron-Frobenius theorem (invited talk paper).
CPP
Jose Divasón, Sebastiaan J. C. Joosten, Ondrej Kuncar, René Thiemann, Akihisa Yamada
2018 J jnl
Safety and conservativity of definitions in HOL and Isabelle/HOL.
Proc. ACM Program. Lang.
Ondrej Kuncar, Andrei Popescu
2017 A conf
Comprehending Isabelle/HOL's Consistency.
ESOP
Ondrej Kuncar, Andrei Popescu
2017 — conf
Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic.
FroCoS
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
2016 B conf
From Types to Sets by Local Type Definitions in Higher-Order Logic.
ITP
Ondrej Kuncar, Andrei Popescu
2016 J jnl
Perron-Frobenius Theorem for Spectral Radius Analysis.
Arch. Formal Proofs
Jose Divasón, Ondrej Kuncar, René Thiemann, Akihisa Yamada
2016 — —
Types, Abstraction and Parametric Polymorphism in Higher-Order Logic.
Ondrej Kuncar
2015 B conf
A Consistent Foundation for Isabelle/HOL.
ITP
Ondrej Kuncar, Andrei Popescu
2015 B conf
Correctness of Isabelle's Cyclicity Checker: Implementability of Overloading in Proof Assistants.
CPP
Ondrej Kuncar
2013 B conf
Data Refinement in Isabelle/HOL.
ITP
Florian Haftmann, Alexander Krauss, Ondrej Kuncar, Tobias Nipkow
2013 B conf
Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL.
CPP
Brian Huffman, Ondrej Kuncar
2011 B conf
Proving Valid Quantified Boolean Formulas in HOL Light.
ITP
Ondrej Kuncar