@Article{ckjujv-synasc17,
  author    = {Cezary Kaliszyk and Josef Urban and Ji\v{r}\'{\i} Vysko\v{c}il},
  title     = {System Description: Statistical Parsing of Informalized
Mizar Formulas},
  booktitle = {SYNASC 2017},
  year =         {2017},
  note =      {to appear},
}



@Article{tgck-jsc17,
  author =       {Thibault Gauthier and Cezary Kaliszyk},
  title =        {Aligning Concepts across Proof Assistant Libraries},
  journal =      {J. Symbolic Computation},
  year =         {2017},
  note =      {to appear},
}


@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     = {Monte Carlo 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{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},
  bibsource = {EasyChair, http://www.easychair.org},
  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},
  bibsource = {EasyChair, http://www.easychair.org},
  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 Coq (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},
  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},
  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)},
}