@article{spjpck-jlc21,
  author    = {Purgał, Stanisław and Parsert, Julian and Kaliszyk, Cezary},
  title     = {A study of continuous vector representations for theorem proving},
  journal   = {Journal of Logic and Computation},
  month = {02},
  year = {2021},
  issn = {0955-792X},
  doi = {10.1093/logcom/exab006},
  url = {https://doi.org/10.1093/logcom/exab006},
}


@article{tgckjurkmn-jar21,
  author    = {Thibault Gauthier and
               Cezary Kaliszyk and
               Josef Urban and
               Ramana Kumar and
               Michael Norrish},
  title     = {{TacticToe}: {L}earning to Prove with Tactics},
  journal   = {J. Autom. Reason.},
  volume    = {65},
  number    = {2},
  pages     = {257--286},
  year      = {2021},
  url       = {https://doi.org/10.1007/s10817-020-09580-x},
  doi       = {10.1007/s10817-020-09580-x},
}


@article{mfckju-jar21,
  author    = {Michael F{\"{a}}rber and
               Cezary Kaliszyk and
               Josef Urban},
  title     = {Machine Learning Guidance for Connection Tableaux},
  journal   = {J. Autom. Reason.},
  volume    = {65},
  number    = {2},
  pages     = {287--320},
  year      = {2021},
  url       = {https://doi.org/10.1007/s10817-020-09576-7},
  doi       = {10.1007/s10817-020-09576-7},
}


@inproceedings{lzlbbppcckju-cicm21,
  author    = {Liao Zhang and Lasse Blaauwbroek and Bartosz Piotrowski and Prokop \v{C}ern\'{y} and Cezary Kaliszyk and Josef Urban},
  title     = {Online Machine Learning Techniques for {C}oq: A Comparison},
  booktitle = {Intelligent Computer Mathematics (CICM 2021)},
  year      = {2021},
  series    = {LNCS},
  editor    = {Fairouz Kamareddine and Claudio Sacerdoti-Coen},
  url       = {https://doi.org/10.1007/978-3-030-81097-9\_5},
  doi       = {10.1007/978-3-030-81097-9\_5},
}


@inproceedings{dmck-iclr21,
  author    = {Dennis M\"{u}ller and Cezary Kaliszyk},
  title     = {Disambiguating Symbolic Expressions in Informal Documents},
  booktitle = {9th International Conference on Learning Representations, {ICLR} 2021},
  year      = {2021},
  url       = {https://openreview.net/forum?id=K5j7D81ABvt},
}


@inproceedings{zzachmckju-tableaux21,
  author    = {Zsolt Zombori and Adrián Csiszárik and Henryk Michalewski and Cezary Kaliszyk and Josef Urban},
  title     = {Towards Finding Longer Proofs},
  booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2021)},
  year      = {2021},
  series    = {LNCS},
  editor    = {Anupam Das and Sara Negri},
  url = {https://doi.org/10.1007/978-3-030-86059-2_10},
  doi = {10.1007/978-3-030-86059-2_10},
}


@article{jjck-mcs20,
  author    = {Jan Jakubuv and Cezary Kaliszyk},
  title     = {Relaxed Weighted Path Order in Theorem Proving},
  journal   = {Math. Comput. Sci.},
  volume    = {14},
  number    = {3},
  pages     = {657--670},
  year      = {2020},
  url       = {https://doi.org/10.1007/s11786-020-00474-0},
  doi       = {10.1007/s11786-020-00474-0},
}


@inproceedings{mockju-ecai20,
  author    = {Miroslav Ols{\'{a}}k and
               Cezary Kaliszyk and
               Josef Urban},
  editor    = {Giuseppe De Giacomo and
               Alejandro Catal{\'{a}} and
               Bistra Dilkina and
               Michela Milano and
               Sen{\'{e}}n Barro and
               Alberto Bugar{\'{\i}}n and
               J{\'{e}}r{\^{o}}me Lang},
  title     = {Property Invariant Embedding for Automated Reasoning},
  booktitle = {{ECAI} 2020 - 24th European Conference on Artificial Intelligence},
  series    = {Frontiers in Artificial Intelligence and Applications},
  volume    = {325},
  pages     = {1395--1402},
  publisher = {{IOS} Press},
  year      = {2020},
  url       = {https://doi.org/10.3233/FAIA200244},
  doi       = {10.3233/FAIA200244},
}



@inproceedings{qwcbckju-cpp20,
  author    = {Qingxiang Wang and
               Chad E. Brown and
               Cezary Kaliszyk and
               Josef Urban},
  editor    = {Jasmin Blanchette and
               Catalin Hritcu},
  title     = {Exploration of neural machine translation in autoformalization of
               mathematics in {M}izar},
  booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
               Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
               20-21, 2020},
  pages     = {85--98},
  publisher = {{ACM}},
  year      = {2020},
  url       = {https://doi.org/10.1145/3372885.3373827},
  doi       = {10.1145/3372885.3373827},
}


@inproceedings{ckfr-cicm20,
  author    = {Cezary Kaliszyk and Florian Rabe},
  title     = {A Survey of Languages for Formalizing Mathematics},
  booktitle = {Intelligent Computer Mathematics (CICM 2020)},
  year      = {2020},
  series    = {LNCS},
  pages     = {138--156},
  url       = {https://doi.org/10.1007/978-3-030-53518-6\_9},
  doi       = {10.1007/978-3-030-53518-6\_9},
  publisher = {Springer, Cham},
  volume    = {12236},
  editor    = {Benzmueller C., Miller B.},
}


@inproceedings{jpsack-gcai20,
  author    = {Julian Parsert and Stephanie Autherith and Cezary Kaliszyk},
  title     = {Property Preserving Embedding of First-order Logic},
  booktitle = {GCAI 2020. 6th Global Conference on Artificial Intelligence (GCAI 2020)},
  editor    = {Gregoire Danoy and Jun Pang and Geoff Sutcliffe},
  series    = {EPiC Series in Computing},
  volume    = {72},
  pages     = {70--82},
  year      = {2020},
  publisher = {EasyChair},
  url       = {https://easychair.org/publications/paper/Cwgq},
  doi       = {10.29007/18t1}
}


@article{beck-mcs20,
  author    = {Burak Ekici and
               Cezary Kaliszyk},
  title     = {{M}ac {L}ane's Comparison Theorem for the {K}leisli Construction Formalized
               in {C}oq},
  journal   = {Math. Comput. Sci.},
  volume    = {14},
  number    = {3},
  pages     = {533--549},
  year      = {2020},
  url       = {https://doi.org/10.1007/s11786-020-00450-8},
  doi       = {10.1007/s11786-020-00450-8},
}


@Article{tgck-jsc19,
  author =       {Thibault Gauthier and Cezary Kaliszyk},
  title =        {Aligning Concepts across Proof Assistant Libraries},
  journal =      {J. Symbolic Computation},
  volume    = {90},
  pages     = {89--123},
  year      = {2019},
  url       = {https://doi.org/10.1016/j.jsc.2018.04.005},
  doi       = {10.1016/j.jsc.2018.04.005},
}


@inproceedings{ckkp-itp19,
  author    = {Cezary Kaliszyk and Karol Pąk},
  title     = {Declarative Proof Translation (short paper)},
  booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)},
  year      = {2019},
  series    = {LIPIcs},
  pages     = {35:1--35:7},
  url       = {https://doi.org/10.4230/LIPIcs.ITP.2019.35},
  doi       = {10.4230/LIPIcs.ITP.2019.35},
  editor    = {John Harrison and
               John O'Leary and
               Andrew Tolmach},
  volume    = {141},
}


@inproceedings{cbckkp-itp19,
  author    = {Chad Brown and Cezary Kaliszyk and Karol Pąk},
  title     = {Higher-order {T}arski {G}rothendieck as a Foundation for Formal Proof},
  booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)},
  year      = {2019},
  series    = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  pages     = {9:1--9:16},
  url       = {https://doi.org/10.4230/LIPIcs.ITP.2019.9},
  doi       = {10.4230/LIPIcs.ITP.2019.9},
  editor    = {John Harrison and
               John O'Leary and
               Andrew Tolmach},
  volume    = {141},
}


@inproceedings{mfck-tableaux19,
  author    = {Michael Färber and Cezary Kaliszyk},
  title     = {Certification of Nonclausal Connection Tableaux Proofs},
  booktitle = {28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2019)},
  year      = {2019},
  series    = {LNCS},
  pages     = {21--38},
  url       = {https://doi.org/10.1007/978-3-030-29026-9\_2},
  doi       = {10.1007/978-3-030-29026-9\_2},
  publisher = {Springer},
  volume    = {11714},
  editor    = {Serenella Cerrito and
               Andrei Popescu},
}


@inproceedings{cbtgckgsju-cade19,
  author    = {Chad Brown and Thibault Gauthier and Cezary Kaliszyk and Geoff Sutcliffe and Josef Urban},
  title     = {{GRUNGE:} {A} Grand Unified {ATP} Challenge},
  booktitle = {The 27th International Conference on Automated Deduction (CADE 2019)},
  year      = {2019},
  series    = {LNCS},
  pages     = {123--141},
  editor    = {Pascal Fontaine},
  volume    = {11716},
  publisher = {Springer},
  url       = {https://doi.org/10.1007/978-3-030-29436-6\_8},
  doi       = {10.1007/978-3-030-29436-6\_8},
}



@article{ckkp-jar19,
  author = {Cezary Kaliszyk and Karol P\k{a}k},
  title =        {Semantics of {M}izar as an {I}sabelle Object Logic},
  journal =      {J. Autom. Reasoning},
  year =         {2019},
  url       = {https://doi.org/10.1007/s10817-018-9479-z},
  doi       = {10.1007/s10817-018-9479-z},
  volume    = {63},
  number    = {3},
  pages     = {557--595},
}


@incollection{bpjucbck-lrgsr19,
  title = {Can Neural Networks Learn Symbolic Rewriting?},
  author = {Bartosz Piotrowski and Josef Urban and Chad Brown and Cezary Kaliszyk},
  booktitle = {Learning and Reasoning with Graph-Structured Representations -- ICML 2019 Workshop},
  pages = {1--4},
  year = {2019},
  url = {https://graphreason.github.io/papers/40.pdf}
}


@proceedings{ckebakcsc-cicm19,
  editor    = {Cezary Kaliszyk and
               Edwin Brady and
               Andrea Kohlhase and
               Claudio Sacerdoti Coen},
  title     = {Intelligent Computer Mathematics - 12th International Conference,
               {CICM} 2019, Prague, Czech Republic, July 8-12, 2019, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {11617},
  publisher = {Springer},
  year      = {2019},
  url       = {https://doi.org/10.1007/978-3-030-23250-4},
  doi       = {10.1007/978-3-030-23250-4},
  isbn      = {978-3-030-23249-8},
}


@incollection{ckjuhmmo-nips18,
  title = {Reinforcement Learning of Theorem Proving},
  author = {Kaliszyk, Cezary and Urban, Josef and Michalewski, Henryk and Ol\v{s}\'{a}k, Miroslav},
  booktitle = {Advances in Neural Information Processing Systems 31},
  editor = {S. Bengio and H. Wallach and H. Larochelle and K. Grauman and N. Cesa-Bianchi and R. Garnett},
  pages = {8836--8847},
  year = {2018},
  publisher = {Curran Associates, Inc.},
  url = {http://papers.nips.cc/paper/8098-reinforcement-learning-of-theorem-proving.pdf}
}


@article{lcck-jar18,
  author    = {\L{}ukasz Czajka and Cezary Kaliszyk},
  title     = {Hammer for {C}oq: Automation for Dependent Type Theory},
  journal   = {J. Autom. Reasoning},
  volume    = {61},
  number    = {1-4},
  pages     = {423--453},
  year      = {2018},
  url       = {https://doi.org/10.1007/s10817-018-9458-4},
  doi       = {10.1007/s10817-018-9458-4},
}


@inproceedings{jjck-icms18,
  author    = {Jan Jakubuv and Cezary Kaliszyk},
  title     = {Towards a Unified Ordering for Superposition-Based Automated Reasoning},
  booktitle = {6th International Conference on Mathematical Software (ICMS 2018)},
  pages     = {245--254},
  year      = {2018},
  url       = {https://doi.org/10.1007/978-3-319-96418-8\_29},
  doi       = {10.1007/978-3-319-96418-8\_29},
  editor    = {James H. Davenport and
               Manuel Kauers and
               George Labahn and
               Josef Urban},
  series    = {LNCS},
  volume    = {10931},
  publisher = {Springer},
  year      = {2018},
}



@inproceedings{lcbeck-cicm18,
  author    = {\L{}ukasz Czajka and
               Burak Ekici and
               Cezary Kaliszyk},
  title     = {Concrete Semantics with {C}oq and {CoqH}ammer},
  booktitle = {11th International Conference on Intelligent Computer Mathematics (CICM 2018)},
  pages     = {53--58},
  year      = {2018},
  url       = {https://doi.org/10.1007/978-3-319-96812-4\_5},
  doi       = {10.1007/978-3-319-96812-4\_5},
  editor    = {Florian Rabe and
               William M. Farmer and
               Grant O. Passmore and
               Abdou Youssef},
  series    = {LNCS},
  volume    = {11006},
  publisher = {Springer},
}


@inproceedings{lcbeck-cicm18,
  author    = {\L{}ukasz Czajka and
               Cezary Kaliszyk},
  title     = {{CoqHammer}: Strong Automation for Program Verification},
  booktitle = {Fourth International Workshop on Coq for Programming Languages, CoqPL 2018}
}


@inproceedings{ckkp-cicm18,
  author    = {Cezary Kaliszyk and Karol P\k{a}k},
  title     = {Isabelle Import Infrastructure for the {M}izar Mathematical Library},
  booktitle = {11th International Conference on Intelligent Computer Mathematics (CICM 2018)},
  pages     = {131--146},
  year      = {2018},
  url       = {https://doi.org/10.1007/978-3-319-96812-4\_13},
  doi       = {10.1007/978-3-319-96812-4\_13},
  editor    = {Florian Rabe and
               William M. Farmer and
               Grant O. Passmore and
               Abdou Youssef},
  series    = {LNCS},
  volume    = {11006},
  publisher = {Springer},
}


@inproceedings{qwckju-cicm18,
  author    = {Qingxiang Wang and
               Cezary Kaliszyk and
               Josef Urban},
  title     = {First Experiments with Neural Translation of Informal to Formal Mathematics},
  booktitle = {11th International Conference on Intelligent Computer Mathematics (CICM 2018)},
  pages     = {255--270},
  year      = {2018},
  url       = {https://doi.org/10.1007/978-3-319-96812-4\_22},
  doi       = {10.1007/978-3-319-96812-4\_22},
  editor    = {Florian Rabe and
               William M. Farmer and
               Grant O. Passmore and
               Abdou Youssef},
  series    = {LNCS},
  volume    = {11006},
  publisher = {Springer},
}



@inproceedings{jpck-itp18,
  author    = {Julian Parsert and
               Cezary Kaliszyk},
  title     = {Towards Formal Foundations for Game Theory},
  booktitle = {Interactive Theorem Proving - 9th International Conference, {ITP} 2018},
  pages     = {495--503},
  year      = {2018},
  doi       = {10.1007/978-3-319-94821-8\_29},
  url       = {https://doi.org/10.1007/978-3-319-94821-8\_29},
  editor    = {Jeremy Avigad and
               Assia Mahboubi},
  series    = {LNCS},
  volume    = {10895},
  publisher = {Springer},
}


@inproceedings{jpck-cpp18,
  author    = {Julian Parsert and Cezary Kaliszyk},
  title     = {Formal Microeconomic Foundations and the {First Welfare Theorem}},
  booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} Conference on Certified Programs
               and Proofs (CPP 2018)},
  doi       = {10.1145/3167100},
  url       = {http://doi.acm.org/10.1145/3167100},
  pages     = {91-101},
  year      = {2018},
  editor    = {June Andronick and Amy P. Felty},
  publisher = {{ACM}},
}



@article{fksu-aicomm18,
  author    = {Pascal Fontaine and
               Cezary Kaliszyk and
               Stephan Schulz and
               Josef Urban},
  title     = {Foreword to the Special Issue on Automated Reasoning},
  journal   = {{AI} Commun.},
  volume    = {31},
  number    = {3},
  pages     = {235--236},
  year      = {2018},
  url       = {https://doi.org/10.3233/AIC-180765},
  doi       = {10.3233/AIC-180765},
}



@inproceedings{ckkp-macis17,
  author    = {Cezary Kaliszyk and Karol Pak},
  title     = {Isabelle Formalization of Set Theoretic Structures and Set Comprehensions},
  pages     = {163--178},
  doi       = {10.1007/978-3-319-72453-9\_12},
  booktitle = {International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS 2017)},
  year      = {2017},
  editor    = {Blömer J. and Kotsireas I. and Kutsia T. and Simos D.},
  series    = {LNCS},
  volume    = {10693},
  publisher = {Springer},
}


@inproceedings{ckjujv-synasc17,
  author    = {Cezary Kaliszyk and Josef Urban and Ji\v{r}\'{\i} Vysko\v{c}il},
  title     = {System Description: Statistical Parsing of Informalized {M}izar Formulas},
  editor = {Tudor Jebelean and Viorel Negru and Dana Petcu and Daniela Zaharie and Tetsuo Ida and Stephen M. Watt},
  booktitle = {19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2017},
  year =         {2017},
  publisher = {{IEEE} Computer Society},
  pages = {169--172},
}


@article{thetal-pi17,
  title={A Formal Proof of the {K}epler conjecture},
  volume={5},
  doi={10.1017/fmp.2017.1},
  journal={Forum of Mathematics, Pi},
  publisher={Cambridge University Press},
  author={
    THOMAS HALES and
    MARK ADAMS and
    GERTRUD BAUER and
    TAT DAT DANG and
    JOHN HARRISON and
    LE TRUONG HOANG and
    CEZARY KALISZYK and
    VICTOR MAGRON and
    SEAN MCLAUGHLIN and
    TAT THANG NGUYEN and
    QUANG TRUONG NGUYEN and
    TOBIAS NIPKOW and
    STEVEN OBUA and
    JOSEPH PLESO and
    JASON RUTE and
    ALEXEY SOLOVYEV and
    THI HOAI AN TA and
    NAM TRUNG TRAN and
    THI DIEP TRIEU and
    JOSEF URBAN and
    KY VU and
    ROLAND ZUMKELLER},
  year={2017}
}


@inproceedings{ckjujv-itp17,
  author    = {Cezary Kaliszyk and Josef Urban and Ji\v{r}\'{\i} Vysko\v{c}il},
  title     = {Automating Formalization by Statistical and Semantic Parsing of Mathematics},
  booktitle = {8th International Conference on Interactive Theorem Proving (ITP 2017)},
  pages     = {12--27},
  year      = {2017},
  url       = {https://doi.org/10.1007/978-3-319-66107-0\_2},
  doi       = {10.1007/978-3-319-66107-0\_2},
  editor    = {Mauricio Ayala{-}Rinc{\'{o}}n and C{\'{e}}sar A. Mu{\~{n}}oz},
  series    = {Lecture Notes in Computer Science},
  volume    = {10499},
  publisher = {Springer},
}


@inproceedings{mfckju-cade17,
  author    = {Michael F{\"{a}}rber and
               Cezary Kaliszyk and
               Josef Urban},
  title     = {{M}onte {C}arlo Tableau Proof Search},
  booktitle = {26th International Conference on Automated Deduction (CADE 2017)},
  pages     = {563--579},
  year      = {2017},
  url       = {https://doi.org/10.1007/978-3-319-63046-5\_34},
  doi       = {10.1007/978-3-319-63046-5\_34},
  editor    = {Leonardo de Moura},
  series    = {LNCS},
  volume    = {10395},
  publisher = {Springer},
}



@inproceedings{ckfccs-iclr17,
  author    = {Cezary Kaliszyk and
               Fran{\c{c}}ois Chollet and
               Christian Szegedy},
  title     = {{HolStep}: {A} Machine Learning Dataset for Higher-order Logic Theorem
               Proving},
  booktitle = {5th International Conference on Learning Representations, {ICLR} 2017,
               Toulon, France, April 24-26, 2017, Conference Track Proceedings},
  year      = {2017},
  url       = {https://openreview.net/forum?id=ryuxYmvel},
}



@inproceedings{slgicsck-lpar17,
  author    = {Sarah Loos and Geoffrey Irving and Christian Szegedy and Cezary Kaliszyk},
  title     = {Deep Network Guided Proof Search},
  booktitle = {LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
  editor    = {Thomas Eiter and David Sands},
  series    = {EPiC Series in Computing},
  volume    = {46},
  pages     = {85--105},
  year      = {2017},
  publisher = {EasyChair},
  url       = {https://doi.org/10.29007/8mwc},
  doi       = {10.29007/8mwc},
  issn      = {2398-7340}}


@inproceedings{tgckju-lpar17,
  author    = {Thibault Gauthier and Cezary Kaliszyk and Josef Urban},
  title     = {{TacticToe}: Learning to Reason with {HOL4} Tactics},
  booktitle = {LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
  editor    = {Thomas Eiter and David Sands},
  series    = {EPiC Series in Computing},
  volume    = {46},
  pages     = {125--143},
  year      = {2017},
  publisher = {EasyChair},
  url       = {https://doi.org/10.29007/ntlb},
  doi       = {10.29007/ntlb},
  issn      = {2398-7340}}


@inproceedings{ckkp-fedcsis17,
  author    = {Cezary Kaliszyk and
               Karol P\k{a}k},
  title     = {Progress in the Independent Certification of {M}izar {M}athematical {L}ibrary
               in {I}sabelle},
  booktitle = {Proceedings of the 2017 Federated Conference on Computer Science and
               Information Systems, FedCSIS 2017},
  pages     = {227--236},
  url       = {https://doi.org/10.15439/2017F289},
  doi       = {10.15439/2017F289},
  editor    = {Maria Ganzha and
               Leszek A. Maciaszek and
               Marcin Paprzycki},
  year      = {2017},
}


@inproceedings{ckkp-cicm17,
  author    = {Cezary Kaliszyk and Karol Pak},
  title     = {Presentation and Manipulation of {M}izar Properties in an {I}sabelle Object Logic},
  pages     = {193--207},
  doi       = {10.1007/978-3-319-62075-6\_14},
  booktitle = {10th International Conference on Intelligent Computer Mathematics (CICM'17)},
  year      = {2017},
  editor    = {Herman Geuvers and
               Matthew England and
               Osman Hasan and
               Florian Rabe and
               Olaf Teschke},
  series    = {LNCS},
  volume    = {10383},
  publisher = {Springer},
}


@inproceedings{dmtgckmkfr-cicm17,
  author    = {Dennis M{\"{u}}ller and
               Thibault Gauthier and
               Cezary Kaliszyk and
               Michael Kohlhase and
               Florian Rabe},
  title     = {Classification of Alignments Between Concepts of Formal Mathematical
               Systems},
  booktitle = {10th International Conference on Intelligent Computer Mathematics (CICM'17)},
  pages     = {83--98},
  year      = {2017},
  doi       = {10.1007/978-3-319-62075-6\_7},
  editor    = {Herman Geuvers and
               Matthew England and
               Osman Hasan and
               Florian Rabe and
               Olaf Teschke},
  series    = {LNCS},
  volume    = {10383},
  publisher = {Springer},
}



@article{jbdgckdkju-jar-mash16,
  author    = {Jasmin Christian Blanchette and
               David Greenaway and
               Cezary Kaliszyk and
               Daniel K{\"{u}}hlwein and
               Josef Urban},
  title     = {A Learning-Based Fact Selector for {Isabelle/HOL}},
  journal   = {J. Autom. Reasoning},
  volume    = {57},
  number    = {3},
  pages     = {219--244},
  year      = {2016},
  url       = {http://dx.doi.org/10.1007/s10817-016-9362-8},
  doi       = {10.1007/s10817-016-9362-8},
}


@article{jbcklpju-h4qed-jfr,
  author = {Jasmin C. Blanchette and Cezary Kaliszyk and Lawrence C. Paulson and Josef Urban},
  title = {Hammering towards {QED}},
  journal = {J. Formalized Reasoning},
  volume = {9},
  number = {1},
  year = {2016},
  issn = {1972-5787},
  url = {http://jfr.unibo.it/article/view/4593},
  doi = {10.6092/issn.1972-5787/4593},
  pages = {101--148}
}


@inproceedings{dack-fase16,
  author    = {David Aspinall and Cezary Kaliszyk},
  title     = {Towards Formal Proof Metrics},
  booktitle = {19th International Conference on Fundamental Approaches to Software Engineering (FASE 2016)},
  pages     = {325--341},
  year      = {2016},
  editor    = {Perdita Stevens and Andrzej Wasowski},
  series    = {Lecture Notes in Computer Science},
  volume    = {9633},
  publisher = {Springer},
  doi       = {10.1007/978-3-662-49665-7\_19},
}


@inproceedings{dack-itp16,
  author    = {David Aspinall and Cezary Kaliszyk},
  title     = {What’s in a Theorem Name? (Rough Diamond)},
  booktitle = {7th Conference on Interactive Theorem Proving (ITP 2016)},
  pages     = {459--465},
  doi       = {10.1007/978-3-319-43144-4\_28},
  editor    = {Jasmin Blanchette and Stephan Merz},
  series    = {LNCS},
  publisher = {Springer},
  volume    = {9807},
  year      = {2016},
}


@inproceedings{ckkpju-cpp16,
  author    = {Cezary Kaliszyk and Karol P\k{a}k and Josef Urban},
  title     = {Towards a {M}izar Environment for {I}sabelle: Foundations and Language},
  booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs
               and Proofs (CPP 2016)},
  doi       = {10.1145/2854065.2854070},
  pages     = {58--65},
  year      = {2016},
  editor    = {Jeremy Avigad and Adam Chlipala},
  publisher = {{ACM}},
}


@inproceedings{ckgsfr-paar16,
  author    = {Cezary Kaliszyk and
               Geoff Sutcliffe and
               Florian Rabe},
  title     = {{TH1:} The {TPTP} Typed Higher-Order Form with Rank-1 Polymorphism},
  pages     = {41--55},
  booktitle = {Proc. 5th Workshop on Practical Aspects of Automated Reasoning (PAAR 2016)},
  year      = {2016},
  editor    = {Pascal Fontaine and
               Stephan Schulz and
               Josef Urban},
  series    = {{CEUR}},
  volume    = {1635},
  publisher = {CEUR-WS.org},
}


@inproceedings{mfck-paar16,
  author    = {Michael F{\"{a}}rber and
               Cezary Kaliszyk},
  title     = {No Choice: Reconstruction of First-order {ATP} Proofs without Skolem Functions},
  pages     = {24--31},
  booktitle = {Proc. 5th Workshop on Practical Aspects of Automated Reasoning (PAAR 2016)},
  year      = {2016},
  editor    = {Pascal Fontaine and
               Stephan Schulz and
               Josef Urban},
  series    = {{CEUR}},
  volume    = {1635},
  publisher = {CEUR-WS.org},
}



@inproceedings{tgckju-cicm16,
  author    = {Thibault Gauthier and
               Cezary Kaliszyk and
               Josef Urban},
  title     = {Initial Experiments with Statistical Conjecturing over Large Formal
               Corpora},
  pages     = {219--228},
  year      = {2016},
  editor    = {Andrea Kohlhase and
               Paul Libbrecht and
               Bruce R. Miller and
               Adam Naumowicz and
               Walther Neuper and
               Pedro Quaresma and
               Frank Wm. Tompa and
               Martin Suda},
  booktitle     = {Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral
               Program, and Work in Progress at the Conference on Intelligent Computer
               Mathematics 2016 (CICM-WiP 2016)},
  series    = {{CEUR}},
  volume    = {1785},
  publisher = {CEUR-WS.org},
}


@inproceedings{ckmkdmfr-cicm16,
  author    = {Cezary Kaliszyk and
               Michael Kohlhase and
               Dennis M{\"{u}}ller and
               Florian Rabe},
  title     = {A Standard for Aligning Mathematical Concepts},
  pages     = {229--244},
  year      = {2016},
  editor    = {Andrea Kohlhase and
               Paul Libbrecht and
               Bruce R. Miller and
               Adam Naumowicz and
               Walther Neuper and
               Pedro Quaresma and
               Frank Wm. Tompa and
               Martin Suda},
  booktitle     = {Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral
               Program, and Work in Progress at the Conference on Intelligent Computer
               Mathematics 2016 (CICM-WiP 2016)},
  series    = {{CEUR}},
  volume    = {1785},
  publisher = {CEUR-WS.org},
}


@inproceedings{ckju-swcs16,
  author    = {Cezary Kaliszyk and
               Josef Urban},
  title     = {Wikis and Collaborative Systems for Large Formal Mathematics},
  booktitle = {Semantic Web Collaborative Spaces},
  pages     = {35--52},
  doi       = {10.1007/978-3-319-32667-2\_3},
  editor    = {Pascal Molli and
               John G. Breslin and
               Maria{-}Esther Vidal},
  series    = {LNCS},
  volume    = {9507},
  publisher = {Springer},
  year      = {2016},
}


@inproceedings{lcck-hatt16,
  author    = {\L{}ukasz Czajka and
               Cezary Kaliszyk},
  title     = {Goal Translation for a Hammer for {C}oq (Extended Abstract)},
  booktitle = {Proceedings First International Workshop on Hammers for Type Theories (HaTT 2016)},
  pages     = {13--20},
  year      = {2016},
  doi       = {10.4204/EPTCS.210.4},
  editor    = {Jasmin Blanchette and
               Cezary Kaliszyk},
  series    = {{EPTCS}},
  volume    = {210},
}


@article{ckju-miz40-jar15,
  author    = {Cezary Kaliszyk and
               Josef Urban},
  title     = {{MizAR} 40 for {M}izar 40},
  journal   = {J. Autom. Reasoning},
  volume    = {55},
  number    = {3},
  pages     = {245--256},
  year      = {2015},
  url       = {http://dx.doi.org/10.1007/s10817-015-9330-8},
  doi       = {10.1007/s10817-015-9330-8},
}


@article{ckju-jsc15,
  author    = {Cezary Kaliszyk and Josef Urban},
  title     = {Learning-assisted Theorem Proving with Millions of Lemmas},
  journal   = {Journal of Symbolic Computation},
  volume    = {69},
  pages     = {109-128},
  year      = {2015},
  doi       = {10.1016/j.jsc.2014.09.032},
}


@article{ckju-mcs-hh,
  author    = {Cezary Kaliszyk and Josef Urban},
  title     = {{HOL(y)Hammer}: Online {ATP} Service for {HOL Light}},
  journal   = {Mathematics in Computer Science},
  volume    = {9},
  number    = {1},
  pages     = {5--22},
  year      = {2015},
  url       = {https://doi.org/10.1007/s11786-014-0182-0},
  doi       = {10.1007/s11786-014-0182-0},
}


@inproceedings{ckjujv-itp15,
  author =       {Cezary Kaliszyk and Josef Urban and Ji\v{r}\'{\i} Vysko\v{c}il},
  title =        {Learning To Parse on Aligned Corpora (Rough Diamond)},
  booktitle =    {Proc. 6h Conference on Interactive Theorem Proving (ITP'15)},
  editor =       {Christian Urban and Xingyuan Zhang},
  series =       {LNCS},
  volume =       {9236},
  pages =        {227-233},
  year =         2015,
  doi =          {10.1007/978-3-319-22102-1\_15},
  publisher =    {Springer-Verlag},
}


@InProceedings{mfck-frocos15,
  author =       {Michael F\"arber and Cezary Kaliszyk},
  title =        {Random Forests for Premise Selection},
  booktitle = {Frontiers of Combining Systems (FroCoS'15)},
  year =      2015,
  editor =    {Carsten Lutz and Silvio Ranise},
  series =    {LNCS},
  pages = {325-340},
  volume = {9322},
  publisher= {Springer},
  doi = {10.1007/978-3-319-24246-0\_20},
}


@InProceedings{ckjujv-frocos15,
  author =       {Cezary Kaliszyk and Josef Urban and Ji\v{r}\'{\i} Vysko\v{c}il},
  title =        {Lemmatization for Stronger Reasoning in Large Theories},
  booktitle = {Frontiers of Combining Systems (FroCoS'15)},
  year =      2015,
  editor =    {Carsten Lutz and Silvio Ranise},
  series =    {LNCS},
  pages = {341-356},
  volume = {9322},
  publisher= {Springer},
  doi="10.1007/978-3-319-24246-0\_21",
}


@inproceedings{ck-tableaux15,
  author =       {Cezary Kaliszyk},
  title =        {Efficient Low-Level Connection Tableaux},
  booktitle =    {Proc. 24th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'15)},
  editor =       {Hans De Nivelle},
  series =       {LNCS},
  volume =       {9323},
  pages =        {102-111},
  year =         2015,
  doi =          {10.1007/978-3-319-24312-2\_8},
  publisher =    {Springer-Verlag},
}


@inproceedings{ckjujv-cpp15,
  author =       {Cezary Kaliszyk and Josef Urban and Jiří Vyskočil},
  title =        {Certified Connection Tableaux Proofs for {HOL L}ight and {TPTP}},
  booktitle = {Proc. of the 4th Conference on Certified Programs and Proofs (CPP'15)},
  editor = {Xavier Leroy and Alwen Tiu},
  isbn      = {978-1-4503-3296-5},
  pages = {59-66},
  year =         2015,
  doi = {10.1145/2676724.2693176},
  publisher = {{ACM}}
}


@inproceedings{tgck-cpp15,
  author =       {Thibault Gauthier and Cezary Kaliszyk},
  title =        {Premise Selection and External Provers for {HOL4}},
  booktitle = {Proc. of the 4th Conference on Certified Programs and Proofs (CPP'15)},
  editor = {Xavier Leroy and Alwen Tiu},
  isbn      = {978-1-4503-3296-5},
  pages = {49-57},
  year =         2015,
  doi = {10.1145/2676724.2693173},
  publisher = {{ACM}}
}


@inproceedings{ckjujv-ijcai15,
  author    = {Cezary Kaliszyk and Josef Urban and Ji\v{r}\'{\i} Vysko\v{c}il},
  title     = {Efficient Semantic Features for Automated Reasoning over Large Theories},
  booktitle = {Proc. of the 24th International Joint Conference on Artificial Intelligence (IJCAI'15)},
  editor    = {Qiang Yang and Michael Wooldridge},
  publisher = {{AAAI} Press},
  year      = {2015},
  pages = {3084--3090},
}


@inproceedings{ckssjujv-cade15,
  author =       {Cezary Kaliszyk and Stephan Schulz and Josef Urban and Ji\v{r}\'i Vysko\v{c}il},
  title =        {System Description: {E.T.} 0.1},
  booktitle =    {Proc. of 25th International Conference on Automated Deduction (CADE'15)},
  editor =       {Amy P. Felty and Aart Middeldorp},
  series =       {LNCS},
  volume =       {9195},
  pages =        {389-398},
  year =         2015,
  doi =          {10.1007/978-3-319-21401-6\_27},
  publisher =    {Springer-Verlag},
}


@inproceedings{ckjuusskcdst-cicm15,
  author =       {Cezary Kaliszyk and Josef Urban and Umair Siddique and Sanaz Khan Afshar and Cvetan Dunchev and Sofi{\`{e}}ne Tahar},
  title =        {Formalizing Physics: Automation, Presentation and Foundation Issues},
  booktitle =    {Proc. of the 8th Conference on Intelligent Computer Mathematics (CICM'15)},
  editor =       {Manfred Kerber and Jacques Carette and Cezary Kaliszyk and Florian Rabe and Volker Sorge},
  series =       {LNCS},
  volume =       {9150},
  pages =        {288-295},
  year =         2015,
  doi =          {10.1007/978-3-319-20615-8\_19},
  publisher =    {Springer-Verlag},
}


@inproceedings{ckju-lpar15,
  author    = {Cezary Kaliszyk and
               Josef Urban},
  title     = {{FEMaLeCoP}: Fairly Efficient Machine Learning Connection Prover},
  booktitle = {20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2015)},
  pages     = {88--96},
  year      = {2015},
  editor    = {Martin Davis and
               Ansgar Fehnker and
               Annabelle McIver and
               Andrei Voronkov},
  series    = {Lecture Notes in Computer Science},
  volume    = {9450},
  publisher = {Springer},
  doi       = {10.1007/978-3-662-48899-7\_7},
}


@inproceedings{tgck-lpar15,
  author    = {Thibault Gauthier and
               Cezary Kaliszyk},
  title     = {Sharing {HOL4} and {HOL L}ight Proof Knowledge},
  booktitle = {20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2015)},
  pages     = {372--386},
  year      = {2015},
  editor    = {Martin Davis and
               Ansgar Fehnker and
               Annabelle McIver and
               Andrei Voronkov},
  series    = {Lecture Notes in Computer Science},
  volume    = {9450},
  publisher = {Springer},
  doi       = {10.1007/978-3-662-48899-7\_26},
}


@inproceedings{ckjujv-iwil15,
  author    = {Cezary Kaliszyk and Josef Urban and Ji\v{r}\'{\i} Vysko\v{c}il},
  title     = {Improving Statistical Linguistic Algorithms for Parsing Mathematics},
  booktitle = {The 11th International Workshop on the Implementation of Logics (IWIL'15)},
  editor    = {Boris Konev and Stephan Schulz and Laurent Simon},
  series    = {EasyChair Proceedings in Computing},
  volume    = {40},
  pages     = {27-36},
  year      = {2016},
  publisher = {EasyChair},
}


@inproceedings{mfck-gcai15,
  author    = {Michael F\"arber and Cezary Kaliszyk},
  title     = {Metis-based Paramodulation Tactic for {HOL Light}},
  booktitle = {Global Conference on Artificial Intelligence (GCAI'15)},
  editor    = {Georg Gottlob and Geoff Sutcliffe and Andrei Voronkov},
  doi       = {10.29007/z9mz},
  series    = {EPiC},
  year      = 2015,
  volume    = {36},
  pages     = {127-136},
  publisher = {EasyChair},
}


@proceedings{jbck-hatt16,
  editor    = {Jasmin Blanchette and Cezary Kaliszyk},
  title     = {Proceedings First Workshop on Hammers for Type Theory, HaTT 2016},
  booktitle = {Proceedings First Workshop on Hammers for Type Theory, HaTT 2016},
  series    = {{EPTCS}},
  volume    = {210},
  year      = {2016},
  url       = {http://dx.doi.org/10.4204/EPTCS.210},
  doi       = {10.4204/EPTCS.210},
}


@proceedings{mkjcckfrvs-cicm15,
  editor    = {Manfred Kerber and
               Jacques Carette and
               Cezary Kaliszyk and
               Florian Rabe and
               Volker Sorge},
  title     = {Intelligent Computer Mathematics - International Conference, {CICM}
               2015, Washington, DC, USA, July 13-17, 2015, Proceedings},
  booktitle = {Intelligent Computer Mathematics - International Conference, {CICM}
               2015, Washington, DC, USA, July 13-17, 2015, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {9150},
  publisher = {Springer},
  year      = {2015},
  url       = {http://dx.doi.org/10.1007/978-3-319-20615-8},
  doi       = {10.1007/978-3-319-20615-8},
}


@proceedings{ckap-pxtp15,
  editor    = {Cezary Kaliszyk and
               Andrei Paskevich},
  title     = {Proceedings Fourth Workshop on Proof eXchange for Theorem Proving,
               PxTP 2015, Berlin, Germany, August 2-3, 2015},
  booktitle = {Proceedings Fourth Workshop on Proof eXchange for Theorem Proving,
               PxTP 2015, Berlin, Germany, August 2-3, 2015},
  series    = {{EPTCS}},
  volume    = {186},
  year      = {2015},
  url       = {http://dx.doi.org/10.4204/EPTCS.186},
  doi       = {10.4204/EPTCS.186},
}


@article{ckju-jar14,
  author    = {Cezary Kaliszyk and
               Josef Urban},
  title     = {Learning-Assisted Automated Reasoning with {F}lyspeck},
  journal   = {J. Autom. Reasoning},
  volume    = {53},
  number    = {2},
  pages     = {173--213},
  year      = {2014},
  url       = {https://doi.org/10.1007/s10817-014-9303-3},
  doi       = {10.1007/s10817-014-9303-3},
}


@inproceedings{sjckju-acl214,
  author =       {Sebastiaan Joosten and Cezary Kaliszyk and Josef Urban},
  title =        {Initial Experiments with {TPTP}-style Automated Theorem Provers
               on {ACL2} Problems},
  booktitle = {Proc. of the 12th International Workshop on the ACL2 Theorem
               Prover and its Applications (ACL2'14)},
  editor = {Freek Verbeek and Julien Schmaltz},
  series    = {EPTCS},
  volume    = {152},
  pages = {77-85},
  year = {2014},
  doi = {10.4204/EPTCS.152.6},
}


@inproceedings{cklmju-scss14,
  author    = {Cezary Kaliszyk and Lionel Mamane and Josef Urban},
  title     = {Machine Learning of {C}oq Proof Guidance: First Experiments},
  booktitle = {Symbolic Computation in Software Science (SCSS 2014)},
  editor    = {Temur Kutsia and Andrei Voronkov},
  series    = {EasyChair Proceedings in Computing},
  doi       = {10.29007/lmmg},
  volume    = {30},
  pages     = {27-34},
  year      = {2014},
  publisher = {EasyChair},
}


@inproceedings{tgckckmn-paar14,
  author    = {Thibault Gauthier and Cezary Kaliszyk and Chantal Keller and Michael Norrish},
  title     = {Beagle as a HOL4 external ATP method},
  booktitle = {4th Workshop on Practical Aspects of Automated Reasoning (PAAR-2014)},
  editor    = {Stephan Schulz and Leonardo De Moura and Boris Konev},
  series    = {EasyChair Proceedings in Computing},
  volume    = {31},
  pages     = {50-59},
  year      = {2015},
  publisher = {EasyChair},
}


@inproceedings{ckjujv-paar14,
  author    = {Cezary Kaliszyk and Josef Urban and Ji\v{r}\'i Vysko\v{c}il},
  title     = {Machine Learner for Automated Reasoning 0.4 and 0.5},
  booktitle = {4th Workshop on Practical Aspects of Automated Reasoning (PAAR-2014)},
  editor    = {Stephan Schulz and Leonardo De Moura and Boris Konev},
  series    = {EasyChair Proceedings in Computing},
  volume    = {31},
  pages     = {60-66},
  year      = {2015},
  publisher = {EasyChair},
}


@inproceedings{ckfr-cicm14,
  author =       {Cezary Kaliszyk and Florian Rabe},
  title =        {Towards Knowledge Management for {HOL L}ight},
  booktitle = {Proc. of the 7th Conference on Intelligent Computer Mathematics (CICM'14)},
  editor = {Stephen Watt and James Davenport and Alan Sexton and Petr Sojka and Josef Urban},
  series = {LNCS},
  volume    = {8543},
  pages = {357-372},
  year =         2014,
  doi = {10.1007/978-3-319-08434-3\_26},
  publisher = {Springer Verlag},
}


@inproceedings{tgck-cicm14,
  author =       {Thibault Gauthier and Cezary Kaliszyk},
  title =        {Matching concepts across {HOL} libraries},
  booktitle = {Proc. of the 7th Conference on Intelligent Computer Mathematics (CICM'14)},
  editor = {Stephen Watt and James Davenport and Alan Sexton and Petr Sojka and Josef Urban},
  series = {LNCS},
  volume    = {8543},
  pages = {267-281},
  year =         2014,
  doi = {10.1007/978-3-319-08434-3\_20},
  publisher = {Springer Verlag}
}


@inproceedings{ckjujvhg-cicm14,
  author =       {Cezary Kaliszyk and Josef Urban and Ji\c{r}\'i Vysko\c{c}il and Herman Geuvers},
  title =        {Developing Corpus-based Translation Methods between Informal and Formal Mathematics},
  booktitle = {Proc. of the 7th Conference on Intelligent Computer Mathematics (CICM'14)},
  editor = {Stephen Watt and James Davenport and Alan Sexton and Petr Sojka and Josef Urban},
  series = {LNCS},
  volume    = {8543},
  pages = {435-439},
  year =         2014,
  doi = {10.1007/978-3-319-08434-3\_34},
  publisher = {Springer Verlag}
}


@inproceedings{ckju-lpar13,
  author =       {Cezary Kaliszyk and Josef Urban},
  title =        {Lemma Mining over {HOL Light}},
  booktitle = {Proc. of the 19th International Conference on Logic for
Programming, Artificial Intelligence, and Reasoning (LPAR'13)},
  editor = {Kenneth L. McMillan and Aart Middeldorp and Andrei Voronkov},
  series    = {LNCS},
  volume    = {8312},
  pages = {503-517},
  year = {2013},
  doi = {10.1007/978-3-642-45221-5\_34},
  publisher = {Springer Verlag}
}


@inproceedings{ckju-cicm13,
  author =       {Cezary Kaliszyk and Josef Urban},
  title =        {Automated Reasoning Service for {HOL L}ight},
  booktitle = {Proc. of the 6th Conference on Intelligent Computer Mathematics (CICM'13)},
  publisher = {Springer Verlag},
  series    = {LNCS},
  volume    = {7961},
  pages = {120-135},
  year = {2013},
  editor = {Jacques Carette and David Aspinall and Christoph Lange and Petr Sojka and Wolfgang Windsteiger},
}


@inproceedings{ctckjuhg-cicm13,
  author = {Carst Tankink and Cezary Kaliszyk and Josef Urban and Herman Geuvers},
  title = {Formal Mathematics on Display: A Wiki for {F}lyspeck},
  booktitle = {Proc. of the 6th Conference on Intelligent Computer Mathematics (CICM'13)},
  publisher = {Springer Verlag},
  series    = {LNCS},
  volume    = {7961},
  pages = {152-167},
  year = {2013},
 doi = {10.1007/978-3-642-39320-4\_10},
  editor = {Jacques Carette and David Aspinall and Christoph Lange and Petr Sojka and Wolfgang Windsteiger},
}


@inproceedings{ckju-cade13,
  author =       {Cezary Kaliszyk and Josef Urban},
  title =        {{PRocH}: Proof Reconstruction for {HOL Light}},
  booktitle = {Proc. of the 24th International Conference on Automated Deduction},
  publisher = {Springer Verlag},
  series    = {LNCS},
  volume    = {7898},
  pages = {267-274},
  year = {2013},
  editor = {Maria Paola Bonacina},
}


@inproceedings{ckak-itp13,
  author =       {Cezary Kaliszyk and Alexander Krauss},
  title =        {Scalable {LCF}-style proof translation},
  url        = {http://dx.doi.org/10.1007/978-3-642-39634-2\_7},
  booktitle = {Proc. of the 4th International Conference on Interactive Theorem Proving (ITP'13)},
  publisher = {Springer Verlag},
  series    = {LNCS},
  volume    = {7998},
  pages = {51-66},
  year = {2013},
  editor = {Sandrine Blazy and Christine Paulin-Mohring and David Pichardie},
}


@inproceedings{dkjbckju-itp13,
  author =       {Daniel K\"uhlwein and Jasmin Christian Blanchette and Cezary Kaliszyk and Josef Urban},
  title =        {{MaSh}: Machine Learning for {Sledgehammer}},
  url       = {http://dx.doi.org/10.1007/978-3-642-39634-2\_6},
  booktitle = {Proc. of the 4th International Conference on Interactive Theorem Proving (ITP'13)},
  publisher = {Springer Verlag},
  series    = {LNCS},
  volume    = {7998},
  pages = {35-50},
  year = {2013},
  editor = {Sandrine Blazy and Christine Paulin-Mohring and David Pichardie},
}


@inproceedings{ctckjuhg-itp13,
  author = {Carst Tankink and Cezary Kaliszyk and Josef Urban and Herman Geuvers},
  title = {Communicating Formal Proofs: The Case of {Flyspeck}},
  url       = {http://dx.doi.org/10.1007/978-3-642-39634-2\_32},
  booktitle = {Proc. of the 4th International Conference on Interactive Theorem Proving (ITP'13)},
  publisher = {Springer Verlag},
  series    = {LNCS},
  volume    = {7998},
  pages = {451-456},
  year = {2013},
  editor = {Sandrine Blazy and Christine Paulin-Mohring and David Pichardie},
}


@inproceedings{ckts-pxtp13,
  author    = {Cezary Kaliszyk and Thomas Sternagel},
  title     = {Initial Experiments on Deriving a Complete {HOL} Simplification Set},
  booktitle = {PxTP 2013},
  editor    = {Jasmin Christian Blanchette and Josef Urban},
  series    = {EPiC Series},
  volume    = {14},
  pages     = {77-86},
  year      = {2013},
  publisher = {EasyChair},
  bibsource = {EasyChair, http://www.easychair.org},
  issn      = {2040-557X},
}


@inproceedings{ckju-pxtp13,
  author    = {Cezary Kaliszyk and Josef Urban},
  title     = {Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution},
  booktitle = {PxTP 2013},
  editor    = {Jasmin Christian Blanchette and Josef Urban},
  series    = {EPiC Series},
  volume    = {14},
  pages     = {87-95},
  year      = {2013},
  publisher = {EasyChair},
  bibsource = {EasyChair, http://www.easychair.org},
  issn      = {2040-557X},
}


@inproceedings{fgakck-adg12,
  author    = "Fadoua Ghourabi and Asem Kasem and Cezary Kaliszyk",
  title     = "Algebraic Analysis of {H}uzita's Origami Operations and Their Extensions",
  booktitle = {9th International Workshop on Automated Deduction in
    Geometry (ADG'12), Revised Selected Papers},
  series    = {Lecture Notes in Computer Science},
  volume    = 7993,
  url = {http://dx.doi.org/10.1007/978-3-642-40672-0\_10},
  doi = {10.1007/978-3-642-40672-0\_10},
  pages     = "143-160",
  year      = 2012
}


@article{cuck-lmcs12,
  author    = {Christian Urban and
               Cezary Kaliszyk},
  title     = {General Bindings and Alpha-Equivalence in {N}ominal {I}sabelle},
  journal   = {Logical Methods in Computer Science},
  volume    = {8},
  number    = {2},
  year      = {2012},
  doi       = {10.1007/978-3-642-19718-5\_25},
}


@inproceedings{ckju-paar12,
  author = {Cezary Kaliszyk and Josef Urban},
  title = {Initial Experiments with External Provers and Premise Selection on {HOL Light} Corpora},
  booktitle = {Proceedings of the Third Workshop on Practical Aspects of
     Automated Reasoning (PAAR-2012), Manchester, UK, June 30, 2012},
  volume    = 21,
  pages     = "72--81",
  year      = 2013,
  editor = {Pascal Fontaine and Renate Schmidt and Stephan Schulz},
  publisher = {EasyChair},
  series    = {EasyChair Proceedings in Computing},
}


@proceedings{ckcl-uitp12,
  editor    = {Cezary Kaliszyk and
               Christoph L\"uth},
  title     = {Proceedings 10th International Workshop On User Interfaces for Theorem
               Provers, {UITP} 2012, Bremen, Germany, July 11th, 2012},
  booktitle = {Proceedings 10th International Workshop On User Interfaces for Theorem
               Provers, {UITP} 2012, Bremen, Germany, July 11th, 2012},
  series    = {{EPTCS}},
  volume    = {118},
  year      = {2013},
  url       = {http://dx.doi.org/10.4204/EPTCS.118},
  doi       = {10.4204/EPTCS.118},
}


@InProceedings{ckhb-cpp11,
  author = {Cezary Kaliszyk and Henk Barendregt},
  title = {Reasoning about Constants in Nominal Isabelle,
   or how to Formalize the Second Fixed Point Theorem},
  booktitle = {Proc. of the First International Conference on Certified Programs and Proofs},
  year = {2011},
  pages     = {87-102},
  editor = {Jean-Pierre Jouannaud and Zhong Shao},
  publisher = {Springer Verlag},
  series = {LNCS},
  volume    = {7086},
}


@inproceedings{ckcu-sac11,
  author = {Cezary Kaliszyk and
               Christian Urban},
  title = {Quotients revisited for {I}sabelle/{HOL}},
  booktitle = {Proc. of the 26th ACM Symposium on Applied Computing (SAC'11)},
  year = {2011},
  pages = {1639-1644},
  publisher = {ACM},
  editor = {William C. Chu and W. Eric Wong and Mathew J. Palakal and Chih-Cheng Hung}
}


@inproceedings{cuck-esop11,
  author = {Christian Urban and
               Cezary Kaliszyk},
  title = {General Bindings and Alpha-Equivalence in {N}ominal {I}sabelle},
  year = {2011},
  pages = {480-500},
  booktitle = {Proc. of the 20th European Symposium on Programming (ESOP'11)},
  publisher = {Springer Verlag},
  series = {LNCS},
  volume = {6602},
  editor = {Gilles Barthe}
}


@inproceedings{ckti-cicm11,
  author    = {Cezary Kaliszyk and Tetsuo Ida},
  title     = {Proof Assistant Decision Procedures for Formalizing Origami},
  booktitle = {Proc. of the 18th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning (Calculemus'11)},
  year      = {2011},
  pages     = {45-57},
  editor    = {James H. Davenport and William M. Farmer and Josef Urban and Florian Rabe},
  publisher = {Springer Verlag},
  series    = {LNCS},
  volume    = {6824},
}


@article{cardfin2,
  author = {Kaliszyk, Cezary},
  title = {Counting derangements, counting non bijective functions and the
    birthday problem},
  journal = {Journal of Formalized Mathematics},
  year = 2010,
  volume = {18},
  number = {4},
  pages = {197--200}
}


@inproceedings{wnckfh-plmms10,
  author = {Neuper, Walther and Kaliszyk, Cezary and Haftmann, Florian},
  title = {CTP-based programming languages. {C}onsiderations about an experimental design},
  volume = {44[1/2]},
  booktitle = {Proc. of the ACM SIGSAM International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS'10)},
  year = {2010},
  pages = {27--41},
  series = {SIGSAM Bull.},
  publisher = {ACM},
  editor = {James Davenport and Lucas Dixon}
}


@article{mhckfrfw-adn10,
  author = {Maxim Hendriks and Cezary Kaliszyk and Femke van Raamsdonk and Freek Wiedijk},
  title = {Teaching logic using a state-of-the-art proof assistant},
  journal = {Acta Didactica Napocensia},
  year = {2010},
  volume = {3},
  number = {2},
  pages = {35-48},
  month = {June}
}


@article{ckro-jfr09,
  author = {Cezary Kaliszyk and Russell O'Connor},
  title = {Computing with Classical Real Numbers},
  journal = {Journal of Formalized Reasoning},
  year = {2009},
  volume = {2},
  number = {1},
  doi = {10.6092/issn.1972-5787/1411},
  pages = {27--39}
}


@misc{kaliszyk-habil,
  author = {Cezary Kaliszyk},
  title = {Learning-Assisted Automated Reasoning},
  year = {2016},
  note = {Habilitation thesis, University of Innsbruck},
}


@phdthesis{kaliszyk-phd,
  author = {Cezary Kaliszyk},
  title = {Correctness and Availability. Building Computer Algebra on top of Proof Assistants and making Proof Assistants available over the Web.},
  school = {Radboud University Nijmegen},
  url = {http://cl-informatik.uibk.ac.at/cek/docs/09/kaliszyk_thesis_webdoc.pdf},
  year = {2009}
}


@inproceedings{ckfw-types08,
  author = {Cezary Kaliszyk and
               Freek Wiedijk},
  title = {Merging procedural and declarative proof},
  year = {2008},
  pages = {203--219},
  booktitle = {Proc. of the Types for Proofs and Programs International Conference (TYPES'08)},
  series = {LNCS},
  volume = {5497},
  publisher = {Springer Verlag},
  editor = {Stefano Berardi and Ferruccio Damiani and Ugo de'Liguoro}
}


@inproceedings{kaliszyk-calculemus08,
  author = {Cezary Kaliszyk},
  title = {Automating Side Conditions in Formalized Partial Functions},
  booktitle = {Proc. of the 15th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning (Calculemus'08)},
  year = {2008},
  pages = {300-314},
  publisher = {Springer Verlag},
  series = {LNCS},
  volume = {5144},
  editor = {Serge Autexier and John Campbell and Julio Rubio and Volker Sorge and Masakazu Suzuki and Freek Wiedijk}
}


@inproceedings{pchgckjmfw-semwiki08,
  author = {Pierre Corbineau and
               Herman Geuvers and
               Cezary Kaliszyk and
               James McKinna and
               Freek Wiedijk},
  title = {A Real Semantic Web for Mathematics Deserves a Real Semantics},
  year = {2008},
  booktitle = {Proc. of the 3rd Semantic Wiki Workshop (SemWiki'08)},
  publisher = {CEUR-WS},
  volume = {360},
  editor = {Christoph Lange and Sebastian Schaffert and Hala Skaf-Molli and Max V\"olkel}
}


@techreport{ckfrfwhwmhrv-icis08,
  author = {{Kaliszyk}, Cezary and {Raamsdonk}, Femke van and {Wiedijk}, Freek and {Wupper}, Hanno and {Hendriks}, Maxim and {Vrijer}, Roel de},
  title = {{Deduction using the ProofWeb system}},
  number = {ICIS--R08016},
  month = {September},
  institution = {Radboud University Nijmegen},
  year = {2008},
  research_group = {IS},
  class = {Report}
}


@inproceedings{pcck-mkm07,
  author = {Pierre Corbineau and
               Cezary Kaliszyk},
  title = {Cooperative Repositories for Formal Proofs},
  booktitle = {Proc. of the 6th International Conference on Mathematical Knowledge Management (MKM'07)},
  year = {2007},
  pages = {221-234},
  publisher = {Springer Verlag},
  series = {LNCS},
  volume = {4573},
  editor = {Manuel Kauers and Manfred Kerber and Robert Miner and Wolfgang Windsteiger},
  url       = {http://doi.org/10.1007/978-3-540-73086-6\_19},
  doi       = {10.1007/978-3-540-73086-6\_19},
}


@inproceedings{ckfw-calculemus07,
  author = {Cezary Kaliszyk and
               Freek Wiedijk},
  title = {Certified Computer Algebra on Top of an Interactive Theorem Prover},
  booktitle = {Proc. of the 14th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning (Calculemus'07)},
  year = {2007},
  pages = {94-105},
  publisher = {Springer Verlag},
  series = {LNCS},
  volume = {4573},
  editor = {Manuel Kauers and Manfred Kerber and Robert Miner and Wolfgang Windsteiger}
}


@inproceedings{kaliszyk-uitp06,
  author = {Cezary Kaliszyk},
  title = {Web Interfaces for Proof Assistants},
  booktitle = {Proc. of the Workshop on User Interfaces for Theorem Provers (UITP'06)},
  series = {ENTCS},
  volume = {174[2]},
  year = {2007},
  pages = {49-61},
  editor = {Serge Autexier and Christoph Benzm\"uller}
}


@MastersThesis{kaliszyk-mag-inf05,
  author =       {Cezary Kaliszyk},
  title =        {Modu\l{} komunikacyjny systemu optymalizacji i personalizacji serwis\'ow WWW SIE
        (Communication module of the SIE WWW service optimization and personalization system)},
  school =       {Warsaw University},
  year =         {2005},
  month =     {June},
}


@techreport{kaliszyk-dea05,
  author = {Cezary Kaliszyk},
  institution = {INRIA},
  title = {Validation des preuves par r\'ecurrence implicite avec des outils bas\'es sur
  le calcul des constructions inductives (Validation of implicit recurrence proofs using the calculus of
  inductive constructions)},
  year = {2005},
  month = {June},
  note = {Rapport de DEA}
}


@inproceedings{gakcmgckms-icwe04,
  author = {Grzegorz Andruszkiewicz and
               Krzysztof Ciebiera and
               Marcin Gozdalik and
               Cezary Kaliszyk and
               Mateusz Srebrny},
  title = {SIE - Intelligent Web Proxy Framework},
  year = {2004},
  pages = {373-385},
  publisher = {Springer Verlag},
  series = {LNCS},
  volume = {3140},
  editor = {Nora Koch and Piero Fraternali and Martin Wirsing},
  booktitle = {4th International Conference on Web Engineering (ICWE 2004)},
}