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

firstlastatgmail
GPG key

Cezary Kaliszyk - Publications

2011

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

2010

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   ]
Walther Neuper, Cezary Kaliszyk, and Florian Haftmann. Ctp-based programming languages. Considerations about an experimental design. In Proc. of the 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   ]
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   ]

2009

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   ]
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   ]

2008

Cezary Kaliszyk and Freek Wiedijk. Merging procedural and declarative proof. In Proc. of the Types for Proofs and Programs International Conference (TYPES'08), volume 5497 of Springer Verlag LNCS, pp. 203—219. 2008.
[   BibTeX   |   Publisher's site   |   PDF   ]
Cezary Kaliszyk. Automating side conditions in formalized partial functions. In Proc. of the 15th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning (Calculemus'08), volume 5144 of Springer Verlag LNCS, pp. 300—314. 2008.
[   BibTeX   |   Publisher's site   |   PDF   ]
Pierre Corbineau, Herman Geuvers, Cezary Kaliszyk, James McKinna, and Freek Wiedijk. A real semantic web for mathematics deserves a real semantics. In Proc. of the 3rd Semantic Wiki Workshop (SemWiki'08), volume 360 of CEUR-WS, 2008.
[   BibTeX   |   Publisher's site   |   PDF   ]
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   ]

2007

Cezary Kaliszyk and Freek Wiedijk. Certified computer algebra on top of an interactive theorem prover. In Proc. of the 14th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning (Calculemus'07), volume 4573 of Springer Verlag LNCS, pp. 94—105. 2007.
[   BibTeX   |   Publisher's site   |   PDF   ]
Pierre Corbineau and Cezary Kaliszyk. Cooperative repositories for formal proofs. In Proc. of the 6th International Conference on Mathematical Knowledge Management (MKM'07), volume 4573 of Springer Verlag LNCS, pp. 221—234. 2007.
[   BibTeX   |   Publisher's site   |   PDF   ]
Cezary Kaliszyk. Web interfaces for proof assistants. In Proc. of the 7th Workshop on User Interfaces for Theorem Provers (UITP'06), volume 174[2] of ENTCS, pp. 49—61, 2007.
[   BibTeX   |   PDF   ]

2005

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   ]
Cezary Kaliszyk. Communication module of the SIE WWW service optimization and personalization system. Master dissertation, Warsaw University, 2005.
[   BibTeX   ]

2004

Grzegorz Andruszkiewicz, Krzysztof Ciebiera, Marcin Gozdalik, Cezary Kaliszyk, and Mateusz Srebrny. Sie - intelligent web proxy framework. In Proc. of the 4th International Conference on Web Engineering (ICWE'04), volume 3140 of Springer Verlag LNCS, pp. 373—385. Springer Verlag, 2004.
[   BibTeX   |   Publisher's site   |   PDF   ]

All pdfs provided above are preprints.

Back to top