photo of Cezary Kaliszyk
University of Innsbruck
Office 3M12, ICT building
Technikerstr. 21a/2 6020 Innsbruck Austria

firstlastatgmail
GPG key

PD Dr. Cezary Kaliszyk

Events:

Teaching:

Current graduate students:

  • Michael Färber (PhD) Formalizing and improving premise selection in ITPs and ATPs
  • Thibault Gauthier (PhD) Matching and sharing HOL proof assistant knowledge
  • Mark Adams (external co-sup.) Proof auditing, HOL Zero, Common HOL platform, Tactician
  • Andrew Morris (MSc) Automation for dependently typed programming

Interested in a BSc, MSc, or PhD with me? Please inquire! Example SMB and MSem topics.

Publications:

2017

  1. Thibault Gauthier and Cezary Kaliszyk. Aligning Concepts across Proof Assistant Libraries. J. Symbolic Computation, accepted for publication, 2017.
    [   BibTeX   |   PDF (preprint)   ]
  2. Tom Hales et al. A formal proof of the Kepler conjecture. Forum of Mathematics, Pi journal (5), 2017.
    [   BibTeX   |   arXiv   |   Publisher's site   ]
  3. Cezary Kaliszyk, Josef Urban, and Jiřı́ Vyskočil. Automating Formalization by Statistical and Semantic Parsing of Mathematics. ITP 2017, invited paper.
    [   PDF (preprint)   ]
  4. Michael Färber, Cezary Kaliszyk, and Josef Urban. Monte Carlo Tableau Proof Search. 26th International Conference on Automated Deduction (CADE 2017), volume 10395 of LNCS, pp. 563‒579. 2017.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  5. Cezary Kaliszyk, François Chollet, and Christian Szegedy. HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving. ICLR 2017, accepted.
    [   PDF (preprint)   ]
  6. Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. TacticToe: Learning to reason with HOL4 Tactics. 21st International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2017), volume 46 of EPiC, pp. 125‒143. 2017.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  7. Sarah Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep Network Guided Proof Search. 21st International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2017), volume 46 of EPiC, pp. 85‒105. 2017.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  8. Cezary Kaliszyk and Karol Pąk. Presentation and Manipulation of Mizar Properties in an Isabelle Object Logic. 10th International Conference on Intelligent Computer Mathematics (CICM 2017), volume 10383 of LNCS, pp. 193‒207. 2017.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  9. Dennis Müller, Thibault Gauthier, Cezary Kaliszyk, Michael Kohlhase, and Florian Rabe Classification of Alignments between Concepts of Formal Mathematical Systems. 10th International Conference on Intelligent Computer Mathematics (CICM 2017), volume 10383 of LNCS, pp. 83‒98. 2017.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]

2016

  1. Jasmin Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef Urban. A Learning-Based Fact Selector for Isabelle/HOL. Journal of Automated Reasoning, 57(3), pp. 219‒244, 2016.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  2. Jasmin C. Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, Josef Urban. Hammering towards QED. Journal of Formalized Reasoning, 9(1):101‒148, 2016.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  3. David Aspinall and Cezary Kaliszyk. Towards Formal Proof Metrics. Proc. 19th International Conference on Fundamental Approaches to Software Engineering (FASE'16), volume 9633 of LNCS, pp. 325‒341, 2016.
    [   BibTeX   [   Publisher's site   |   PDF (preprint)   ]
  4. David Aspinall and Cezary Kaliszyk. What’s in a Theorem Name? Proc. 7h Conference on Interactive Theorem Proving (ITP'16), volume 9807 of LNCS, pp. 459‒465, 2016.
  5. [   BibTeX   [   Publisher's site   |   PDF (preprint)   ]
  6. Cezary Kaliszyk, Karol Pąk, and Josef Urban. Towards a Mizar Environment for Isabelle: Foundations and Language. 5th ACM Conference on Certified Programs and Proofs (CPP'16), ACM, pp. 58‒65, 2016.
    [   BibTeX   |   Publisher (openaccess)   |   PDF (preprint)   ]
  7. Cezary Kaliszyk and Josef Urban. Wikis and Collaborative Systems for Large Formal Mathematics. Semantic Web Collaborative Spaces - Revised Selected and Invited Papers, volume 9507 of LNCS, pp. 35‒52, 2016.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  8. Cezary Kaliszyk, Geoff Sutcliffe, and Florian Rabe. TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism. 5th Workshop on Practical Aspects of Automated Reasoning (PAAR'16), volume 1635 of CEUR-WS, pp. 41-55, 2016.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  9. Michael Färber and Cezary Kaliszyk. No Choice: Reconstruction of First-order ATP Proofs without Skolem Functions. 5th Workshop on Practical Aspects of Automated Reasoning (PAAR'16), volume 1635 of CEUR-WS, pp. 23-31, 2016.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  10. Cezary Kaliszyk, Michael Kohlhase, Dennis Mueller, Florian Rabe. A Standard for Aligning Mathematical Concepts. 9th Conference on Intelligent Computer Mathematics Work in Progress (CICM-WiP'16), volume 1785 of CEUR-WS, pp. 229-244, 2016.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  11. Thibault Gauthier, Cezary Kaliszyk, and Josef Urban Initial Experiments with Statistical Conjecturing over Large Formal Corpora. 9th Conference on Intelligent Computer Mathematics Work in Progress (CICM-WiP'16), volume 1785 of CEUR-WS, pp. 219-228, 2016.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  12. Łukasz Czajka and Cezary Kaliszyk. Goal Translation for a Hammer for Coq. 1st International Workshop on Hammers for Type Theories (HaTT 2016), volume 210 of EPTCS, pp. 13‒20, 2016.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]

2015

  1. Cezary Kaliszyk and Josef Urban. MizAR 40 for Mizar 40. Journal of Automated Reasoning, 55(3), pp. 245‒256, 2015.
  2. Cezary Kaliszyk and Josef Urban. Learning-assisted Theorem Proving with Millions of Lemmas. Journal of Symbolic Computation, 69, pp. 109‒128, 2015.
  3. Cezary Kaliszyk and Josef Urban. HOL(y)Hammer: Online ATP Service for HOL Light. Mathematics in Computer Science, 9(1), pp. 5‒22, 2015.
    [   BibTeX   |   PDF (openaccess) |   PDF (preprint)   ]
  4. Cezary Kaliszyk, Josef Urban, Jiří Vyskočil. Learning To Parse on Aligned Corpora. 6h Conference on Interactive Theorem Proving (ITP'15), volume 9236 of LNCS, pp. 227‒233, 2015.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  5. Cezary Kaliszyk, Josef Urban, Jiří Vyskočil. Lemmatization for Stronger Reasoning in Large Theories. Proc. 10th International Symposium on Frontiers of Combining Systems (FroCoS'15), volume 9322 of LNCS, pp. 341‒356, 2015.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  6. Michael Färber, Cezary Kaliszyk. Random Forests for Premise Selection. 10th International Symposium on Frontiers of Combining Systems (FroCoS'15), volume 9322 of LNCS, pp. 325‒340, 2015.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  7. Cezary Kaliszyk. Efficient Low-level Connection Tableaux. Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'15), volume 9323 of LNCS, pp. 102‒111, 2015.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)  ]
  8. Cezary Kaliszyk, Josef Urban, Jiří Vyskočil. Certified Connection Tableaux Proofs for HOL Light and TPTP. 4th Conference on Certified Programs and Proofs (CPP'15), ACM, pp. 59‒66, 2015.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  9. Thibault Gauthier, Cezary Kaliszyk. Premise Selection and External Provers for HOL4. 4th Conference on Certified Programs and Proofs (CPP'15), ACM, pp. 49‒57, 2015.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  10. Cezary Kaliszyk, Josef Urban, Jiří Vyskočil. Efficient Semantic Features for Automated Reasoning over Large Theories. 24th International Joint Conference on Artificial Intelligence (IJCAI'15), AAAI, pp. 3084‒3090, 2015.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  11. Cezary Kaliszyk, Stephan Schulz, Josef Urban, Jiří Vyskočil. System Description: E.T. 0.1. 25th International Conference on Automated Deduction (CADE'15), volume 9195 of LNCS, pp. 389‒398, 2015.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  12. C. Kaliszyk, J. Urban, U. Siddique, S. Khan-Afshar, C. Dunchev, and S. Tahar. Formalizing Physics: Automation, Presentation and Foundation Issues. 8th Conference on Intelligent Computer Mathematics (CICM'15), volume 9150 of LNCS, pp. 288‒295, 2015.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  13. Cezary Kaliszyk and Josef Urban. FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover. Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'15), volume 9450 of LNCS, pp. 88‒96, 2015.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  14. Thibault Gauthier and Cezary Kaliszyk Sharing HOL4 and HOL Light proof knowledge Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'15), volume 9450 of LNCS, pp. 372‒386, 2015.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)  ]
  15. Michael Färber and Cezary Kaliszyk Metis-based Paramodulation Tactic for HOL Light 1st Global Conference on Artificial Intelligence (GCAI'15), volume 36 of EPiC, pp. 127‒136, 2015.
    [   BibTeX   |   Proceedings   |   PDF (preprint)  ]
  16. Cezary Kaliszyk, Josef Urban, Jiří Vyskočil. Improving Statistical Linguistic Algorithms for Parsing Mathematics. 11th International Workshop on the Implementation of Logics (IWIL'15), volume 40 of EPiC, pp. 27-36, 2016.
    [   BibTeX   |   Proceedings   |   PDF (preprint)  ]

2014

  1. Cezary Kaliszyk and Josef Urban. Learning-assisted Automated Reasoning with Flyspeck. Journal of Automated Reasoning, 53(2), pp. 173‒213, 2014.
    [   BibTeX   |   PDF (preprint)   ]
  2. Sebastiaan Joosten, Cezary Kaliszyk, and Josef Urban. Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems. 12th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'14), EPTCS, 152, pp. 77‒85, 2014.
    [   BibTeX   |   arXiv   |   PDF (preprint)   ]
  3. Cezary Kaliszyk, Lionel Mamane, and Josef Urban. Machine Learning of Coq Proof Guidance: First Experiments. 6th International Symposium on Symbolic Computation in Software Science (SCSS'14), volume 30 of EPiC, pp. 27‒34, 2014.
    [   BibTeX   |   Proceedings   |   PDF (preprint)   ]
  4. Thibault Gauthier, Cezary Kaliszyk, Chantal Keller, and Michael Norrish. Beagle as a HOL4 external ATP method. 4th Workshop on Practical Aspects of Automated Reasoning (PAAR'14), volume 31 of EPiC, pp. 50‒59, 2015.
    [   BibTeX   |   Proceedings   |   PDF (preprint)   ]
  5. Cezary Kaliszyk, Josef Urban, and Jiří Vyskočil. Machine Learner for Automated Reasoning 0.4 and 0.5. 4th Workshop on Practical Aspects of Automated Reasoning (PAAR'14), volume 31 of EPiC, pp. 60‒66, 2015.
    [   BibTeX   |   Proceedings   |   PDF (preprint)   ]
  6. Cezary Kaliszyk and Florian Rabe. Towards Knowledge Management for HOL Light. 7th Conference on Intelligent Computer Mathematics (CICM'14), volume 8543 of LNCS, pp. 357‒372, 2014.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  7. Thibault Gauthier and Cezary Kaliszyk. Matching concepts across HOL libraries. 7th Conference on Intelligent Computer Mathematics (CICM'14), volume 8543 of LNCS, pp. 267‒281, 2014.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  8. Cezary Kaliszyk, Josef Urban, Jiří Vyskočil, and Herman Geuvers. Developing Corpus-based Translation Methods between Informal and Formal Mathematics: Project Description. 7th Conference on Intelligent Computer Mathematics (CICM'14), volume 8543 of LNCS, pp. 435‒439, 2014.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]

2013

  1. Cezary Kaliszyk and Josef Urban. Lemma Mining over HOL Light. 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'13), volume 8312 of LNCS, pp. 503‒517. 2013.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  2. Cezary Kaliszyk and Josef Urban. Automated Reasoning Service for HOL Light. 6th Conference on Intelligent Computer Mathematics (CICM'13), volume 7961 of LNCS, pp. 120‒135. 2013.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  3. Carst Tankink, Cezary Kaliszyk, Josef Urban, and Herman Geuvers. Formal Mathematics on Display: A Wiki for Flyspeck. 6th Conference on Intelligent Computer Mathematics (CICM'13), volume 7961 of LNCS, pp. 152‒167, 2013.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  4. Cezary Kaliszyk and Josef Urban. PRocH: Proof Reconstruction for HOL Light. 24th International Conference on Automated Deduction (CADE'13), volume 7898 of LNCS, pp. 267‒274, 2013.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  5. Cezary Kaliszyk and Alexander Krauss. Scalable LCF-style proof translation. 4th International Conference on Interactive Theorem Proving (ITP'13), volume 7998 of LNCS, pp. 51‒66, 2013.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  6. Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, and Josef Urban. MaSh: Machine Learning for Sledgehammer. 4th International Conference on Interactive Theorem Proving (ITP'13), volume 7998 of LNCS, pp. 35‒50, 2013.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  7. Carst Tankink, Cezary Kaliszyk, Josef Urban, and Herman Geuvers. Communicating Formal Proofs: The Case of Flyspeck. 4th International Conference on Interactive Theorem Proving (ITP'13), volume 7998 of LNCS, pp. 451‒456, 2013.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  8. Cezary Kaliszyk, Thomas Sternagel. Initial Experiments on Deriving a Complete HOL Simplification Set. 3rd International Workshop on Proof Exchange for Theorem Proving (PxTP'13), volume 14 of EPiC, pp. 77‒86, 2013.
    [   BibTeX   |   Proceedings   |   PDF (preprint)   ]
  9. Cezary Kaliszyk, Josef Urban. Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution. 3rd International Workshop on Proof Exchange for Theorem Proving (PxTP'13), volume 14 of EPiC, pp. 87‒95, 2013.
    [   BibTeX   |   Proceedings   |   PDF (preprint)   ]

2012

  1. Christian Urban and Cezary Kaliszyk. General Bindings and Alpha-Equivalence in Nominal Isabelle. Logical Methods in Computer Science, 8(2):1‒35, 2012.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  2. Fadoua Ghourabi, Asem Kasem, and Cezary Kaliszyk. Algebraic Analysis of Huzita's Origami Operations and their Extensions. 9th International Workshop on Automated Deduction in Geometry (ADG'12), volume 7993 of LNCS, pp. 143‒160, 2012.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  3. Cezary Kaliszyk and Josef Urban. Initial Experiments with External Provers and Premise Selection on HOL Light Corpora. Third Workshop on Practical Aspects of Automated Reasoning (PAAR'12), volume 21 of EPiC, pp. 72‒81, 2012.
    [   BibTeX   |   Proceedings   |   PDF (preprint)   ]

2011

  1. Cezary Kaliszyk and Henk Barendregt. Reasoning about constants in Nominal Isabelle, or how to formalize the second fixed point theorem. First International Conference on Certified Programs and Proofs (CPP'11), volume 7086 of LNCS, pp. 87‒102, 2011.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  2. Cezary Kaliszyk and Christian Urban. Quotients revisited for Isabelle/HOL. 26th ACM Symposium on Applied Computing (SAC'11), pp. 1639‒1644. ACM, 2011.
    [ BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  3. Christian Urban and Cezary Kaliszyk. General bindings and alpha-equivalence in Nominal Isabelle. 20th European Symposium on Programming (ESOP'11), volume 6602 of LNCS, pp. 480‒500, 2011.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  4. Cezary Kaliszyk and Tetsuo Ida. Proof assistant decision procedures for formalizing origami. 4th Conference on Intelligent Computer Mathematics (CICM'11), volume 6824 of LNCS, 2011.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]

2010 and before

  1. Cezary Kaliszyk. Counting derangements, counting non bijective functions and the birthday problem. Formalized Mathematics, 18(4):197‒200, Mizar Mathematical Library, 2010.
    [   BibTeX   |   MML   |   Abstract   ]
  2. Walther Neuper, Cezary Kaliszyk, and Florian Haftmann. Ctp-based programming languages. Considerations about an experimental design. ACM SIGSAM International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS'10), volume 44[1/2] of SIGSAM Bull., pp. 27‒41. ACM, 2010.
    [   BibTeX   |   Proceedings   |   PDF (preprint)   ]
  3. Maxim Hendriks, Cezary Kaliszyk, Femke van Raamsdonk, and Freek Wiedijk. Teaching logic using a state-of-the-art proof assistant. Acta Didactica Napocensia, 3(2):35‒48, June 2010.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  4. Cezary Kaliszyk and Russell O'Connor. Computing with classical real numbers. Journal of Formalized Reasoning, 2(1):27‒39, 2009.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  5. Cezary Kaliszyk and Freek Wiedijk. Merging procedural and declarative proof. Types for Proofs and Programs International Conference (TYPES'08), volume 5497 of LNCS, pp. 203‒219. 2008.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  6. Cezary Kaliszyk. Automating side conditions in formalized partial functions. 15th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning (Calculemus'08), volume 5144 of LNCS, pp. 300‒314, 2008.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  7. Pierre Corbineau, Herman Geuvers, Cezary Kaliszyk, James McKinna, and Freek Wiedijk. A real semantic web for mathematics deserves a real semantics. 3rd Semantic Wiki Workshop (SemWiki'08), volume 360 of CEUR-WS, 2008.
    [   BibTeX   |   Proceedings   |   PDF (preprint)   ]
  8. Cezary Kaliszyk and Freek Wiedijk. Certified computer algebra on top of an interactive theorem prover. 14th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning (Calculemus'07), volume 4573 of LNCS, pp. 94‒105, 2007.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  9. Pierre Corbineau and Cezary Kaliszyk. Cooperative repositories for formal proofs. 6th International Conference on Mathematical Knowledge Management (MKM'07), volume 4573 of LNCS, pp. 221‒234, 2007.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  10. Cezary Kaliszyk. Web interfaces for proof assistants. 7th Workshop on User Interfaces for Theorem Provers (UITP'06), volume 174[2] of ENTCS, pp. 49‒61, 2007.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]
  11. Grzegorz Andruszkiewicz, Krzysztof Ciebiera, Marcin Gozdalik, Cezary Kaliszyk, and Mateusz Srebrny. Sie - intelligent web proxy framework. 4th International Conference on Web Engineering (ICWE'04), volume 3140 of LNCS, pp. 373‒385. 2004.
    [   BibTeX   |   Publisher's site   |   PDF (preprint)   ]

Theses, proceedings, and other:

  1. Cezary Kaliszyk. Learning-Assisted Automated Reasoning. Habilitation Thesis, accepted February 2016.
    [   BibTeX   |   PDF   ]
  2. Jasmin Blanchette and Cezary Kaliszyk. Proceedings of the 1st Workshop on Hammers for Type Theory (HaTT 2016), volume 210 of EPTCS, 2016.
    [   BibTeX   |   Published   ]
  3. Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge. Proc. of the 8th International Conference on Intelligent Computer Mathematics (CICM 2015), volume 9150 of LNCS, 2015.
    [   BibTeX   |   Published   ]
  4. Cezary Kaliszyk and Andrei Paskevich. Proceedings of the 4th Workshop on Proof Exchange for Theorem Proving (PxTP 2015), volume 186 of EPTCS, 2015.
    [   BibTeX   |   Published   ]
  5. Cezary Kaliszyk and Christoph Lüth. Proceedings of the 10th International Workshop On User Interfaces for Theorem Provers (UITP 2012), volume 118 of EPTCS, 2013.
    [   BibTeX   |   Published   ]
  6. Cezary Kaliszyk. Correctness and Availability. Building Computer Algebra on top of Proof Assistants and making Proof Assistants available over the Web. PhD dissertation, Radboud University Nijmegen, September 2009.
    [   BibTeX   |   Published   |   PDF   ]
  7. Cezary Kaliszyk, Femke van Raamsdonk, Freek Wiedijk, Hanno Wupper, Maxim Hendriks, and Roel de Vrijer. Deduction using the ProofWeb system. Technical Report ICIS-R08016, Radboud University Nijmegen, September 2008.
    [   BibTeX   |   PDF   ]
  8. Cezary Kaliszyk. Validation des preuves par récurrence implicite avec des outils basés sur le calcul des constructions inductives
    (Validation of implicit recurrence proofs using the calculus of inductive constructions).
    Technical report, INRIA, 2005.
    [   BibTeX   |   PDF   ]
  9. Cezary Kaliszyk. Moduł komunikacyjny systemu optymalizacji i personalizacji serwisów WWW SIE
    (Communication module of the SIE WWW service optimization and personalization system).
    Master dissertation, Warsaw University, 2005.
    [   BibTeX   |   PDF   ]