Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDBibTeX records: Ondrej Kuncar
@article{DBLP:journals/jar/KuncarP19,
author = {Ondrej Kuncar and
Andrei Popescu},
title = {From Types to Sets by Local Type Definition in Higher-Order Logic},
journal = {J. Autom. Reason.},
volume = {62},
number = {2},
pages = {237--260},
year = {2019},
url = {https://doi.org/10.1007/s10817-018-9464-6},
doi = {10.1007/S10817-018-9464-6},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/KuncarP19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/KuncarP19a,
author = {Ondrej Kuncar and
Andrei Popescu},
title = {A Consistent Foundation for Isabelle/HOL},
journal = {J. Autom. Reason.},
volume = {62},
number = {4},
pages = {531--555},
year = {2019},
url = {https://doi.org/10.1007/s10817-018-9454-8},
doi = {10.1007/S10817-018-9454-8},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/KuncarP19a.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/pacmpl/Kuncar018,
author = {Ondrej Kuncar and
Andrei Popescu},
title = {Safety and conservativity of definitions in {HOL} and Isabelle/HOL},
journal = {Proc. {ACM} Program. Lang.},
volume = {2},
number = {{POPL}},
pages = {24:1--24:26},
year = {2018},
url = {https://doi.org/10.1145/3158112},
doi = {10.1145/3158112},
timestamp = {Wed, 17 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/pacmpl/Kuncar018.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/DivasonJKT018,
author = {Jose Divas{\'{o}}n and
Sebastiaan J. C. Joosten and
Ondrej Kuncar and
Ren{\'{e}} Thiemann and
Akihisa Yamada},
editor = {June Andronick and
Amy P. Felty},
title = {Efficient certification of complexity proofs: formalizing the Perron-Frobenius
theorem (invited talk paper)},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January
8-9, 2018},
pages = {2--13},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3167103},
doi = {10.1145/3167103},
timestamp = {Mon, 15 Jun 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/DivasonJKT018.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/esop/Kuncar017,
author = {Ondrej Kuncar and
Andrei Popescu},
editor = {Hongseok Yang},
title = {Comprehending Isabelle/HOL's Consistency},
booktitle = {Programming Languages and Systems - 26th European Symposium on Programming,
{ESOP} 2017, Held as Part of the European Joint Conferences on Theory
and Practice of Software, {ETAPS} 2017, Uppsala, Sweden, April 22-29,
2017, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10201},
pages = {724--749},
publisher = {Springer},
year = {2017},
url = {https://doi.org/10.1007/978-3-662-54434-1\_27},
doi = {10.1007/978-3-662-54434-1\_27},
timestamp = {Tue, 14 May 2019 10:00:41 +0200},
biburl = {https://dblp.org/rec/conf/esop/Kuncar017.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/frocos/BiendarraBBDFHK17,
author = {Julian Biendarra and
Jasmin Christian Blanchette and
Aymeric Bouzy and
Martin Desharnais and
Mathias Fleury and
Johannes H{\"{o}}lzl and
Ondrej Kuncar and
Andreas Lochbihler and
Fabian Meier and
Lorenz Panny and
Andrei Popescu and
Christian Sternagel and
Ren{\'{e}} Thiemann and
Dmitriy Traytel},
editor = {Clare Dixon and
Marcelo Finger},
title = {Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic},
booktitle = {Frontiers of Combining Systems - 11th International Symposium, FroCoS
2017, Bras{\'{\i}}lia, Brazil, September 27-29, 2017, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10483},
pages = {3--21},
publisher = {Springer},
year = {2017},
url = {https://doi.org/10.1007/978-3-319-66167-4\_1},
doi = {10.1007/978-3-319-66167-4\_1},
timestamp = {Mon, 28 Aug 2023 21:17:55 +0200},
biburl = {https://dblp.org/rec/conf/frocos/BiendarraBBDFHK17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@phdthesis{DBLP:phd/dnb/Kuncar16,
author = {Ondrej Kuncar},
title = {Types, Abstraction and Parametric Polymorphism in Higher-Order Logic},
school = {Technical University Munich, Germany},
year = {2016},
url = {https://nbn-resolving.org/urn:nbn:de:bvb:91-diss-20160408-1285267-1-5},
urn = {urn:nbn:de:bvb:91-diss-20160408-1285267-1-5},
timestamp = {Sat, 17 Jul 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/phd/dnb/Kuncar16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/afp/DivasonKTY16,
author = {Jose Divas{\'{o}}n and
Ondrej Kuncar and
Ren{\'{e}} Thiemann and
Akihisa Yamada},
title = {Perron-Frobenius Theorem for Spectral Radius Analysis},
journal = {Arch. Formal Proofs},
volume = {2016},
year = {2016},
url = {https://www.isa-afp.org/entries/Perron\_Frobenius.shtml},
timestamp = {Mon, 25 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/afp/DivasonKTY16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/Kuncar016,
author = {Ondrej Kuncar and
Andrei Popescu},
editor = {Jasmin Christian Blanchette and
Stephan Merz},
title = {From Types to Sets by Local Type Definitions in Higher-Order Logic},
booktitle = {Interactive Theorem Proving - 7th International Conference, {ITP}
2016, Nancy, France, August 22-25, 2016, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9807},
pages = {200--218},
publisher = {Springer},
year = {2016},
url = {https://doi.org/10.1007/978-3-319-43144-4\_13},
doi = {10.1007/978-3-319-43144-4\_13},
timestamp = {Tue, 14 May 2019 10:00:37 +0200},
biburl = {https://dblp.org/rec/conf/itp/Kuncar016.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Kuncar15,
author = {Ondrej Kuncar},
editor = {Xavier Leroy and
Alwen Tiu},
title = {Correctness of Isabelle's Cyclicity Checker: Implementability of Overloading
in Proof Assistants},
booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs,
{CPP} 2015, Mumbai, India, January 15-17, 2015},
pages = {85--94},
publisher = {{ACM}},
year = {2015},
url = {https://doi.org/10.1145/2676724.2693175},
doi = {10.1145/2676724.2693175},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Kuncar15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/Kuncar015,
author = {Ondrej Kuncar and
Andrei Popescu},
editor = {Christian Urban and
Xingyuan Zhang},
title = {A Consistent Foundation for Isabelle/HOL},
booktitle = {Interactive Theorem Proving - 6th International Conference, {ITP}
2015, Nanjing, China, August 24-27, 2015, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9236},
pages = {234--252},
publisher = {Springer},
year = {2015},
url = {https://doi.org/10.1007/978-3-319-22102-1\_16},
doi = {10.1007/978-3-319-22102-1\_16},
timestamp = {Tue, 14 May 2019 10:00:37 +0200},
biburl = {https://dblp.org/rec/conf/itp/Kuncar015.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/HuffmanK13,
author = {Brian Huffman and
Ondrej Kuncar},
editor = {Georges Gonthier and
Michael Norrish},
title = {Lifting and Transfer: {A} Modular Design for Quotients in Isabelle/HOL},
booktitle = {Certified Programs and Proofs - Third International Conference, {CPP}
2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8307},
pages = {131--146},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-319-03545-1\_9},
doi = {10.1007/978-3-319-03545-1\_9},
timestamp = {Tue, 14 May 2019 10:00:54 +0200},
biburl = {https://dblp.org/rec/conf/cpp/HuffmanK13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/HaftmannKKN13,
author = {Florian Haftmann and
Alexander Krauss and
Ondrej Kuncar and
Tobias Nipkow},
editor = {Sandrine Blazy and
Christine Paulin{-}Mohring and
David Pichardie},
title = {Data Refinement in Isabelle/HOL},
booktitle = {Interactive Theorem Proving - 4th International Conference, {ITP}
2013, Rennes, France, July 22-26, 2013. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7998},
pages = {100--115},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-642-39634-2\_10},
doi = {10.1007/978-3-642-39634-2\_10},
timestamp = {Mon, 26 Feb 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/itp/HaftmannKKN13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/Kuncar11,
author = {Ondrej Kuncar},
editor = {Marko C. J. D. van Eekelen and
Herman Geuvers and
Julien Schmaltz and
Freek Wiedijk},
title = {Proving Valid Quantified Boolean Formulas in {HOL} Light},
booktitle = {Interactive Theorem Proving - Second International Conference, {ITP}
2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6898},
pages = {184--199},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-22863-6\_15},
doi = {10.1007/978-3-642-22863-6\_15},
timestamp = {Tue, 14 May 2019 10:00:37 +0200},
biburl = {https://dblp.org/rec/conf/itp/Kuncar11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
a service of 
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-02-27 23:41 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
