Publications

Refereed

• Jesús Aransay, Clemens Ballarin and Julio Rubio. A mechanized proof of the Basic Perturbation Lemma.  Journal of Automated Reasoning,  40(4):271–292, 2008.
• Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and Proof Contexts. In J.M. Borwein and W.M. Farmer, MKM 2006, LNAI 4108, pages 31–43, 2006. © Springer.
• Jesús Aransay, Clemens Ballarin and Julio Rubio. Extracting Computer Algebra programs from statements. In R. Moreno-Díaz et al., EUROCAST 2005, Las Palmas, Spain, LNCS 3643, pages 159-168, 2005. © Springer.
• Alessandro Armando and Clemens Ballarin. A reconstruction and extension of Maple's assume facility via constraint contextual rewriting.  Journal of Symbolic Computation, 39(5), 503-521, 2005.
• Jesús Aransay, Clemens Ballarin and Julio Rubio. Four Approaches to Automated Reasoning with Differential Algebraic Structures. In B. Buchberger and J.A. Campbell, AISC 2004, Linz, Austria, LNAI 3249, pages 221-234, 2004. © Springer.
• Clemens Ballarin and Manuel Kauers. Solving Parametric Linear Systems: an Experiment with Constraint Algebraic Programming. ACM SIGSAM Bulletin, 38(2), 33-46, 2004.
• Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar. In Stefano Berardi et al., Types for Proofs and Programs: International Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004. © Springer.
• Alessandro Armando and Clemens Ballarin. Maple's Evaluation Process as Constraint Contextual Rewriting. In Bernardin Mourrain, editor, ISSAC 2001, London, Ontario, Canada, pages 32-37, 2001.
• Clemens Ballarin and Lawrence C. Paulson. A Pragmatic Approach to Extending Provers by Computer Algebra - with Applications to Coding Theory. Fundamenta Informaticae, 39(1, 2), 1-20, 1999.
• Clemens Ballarin and Lawrence C. Paulson. Reasoning about coding theory: The benefits we get from computer algebra. In Jacques Calmet and Jan Plaza, AISC'98: Plattsburgh, New York, USA, September 1998: Proceedings, LNAI 1476, pages 55-66, 1998. © Springer.
• Clemens Ballarin, Karsten Homann and Jacques Calmet. Theorems and algorithms: An interface between Isabelle and Maple. In A. H. M. Levelt, ISSAC '95, Montréal, Canada, pages 150-157. ACM Press, 1995. Available as postscript.

Workshop papers, technical reports and manuscripts

• Clemens Ballarin. Tutorial to Locales and Locale Interpretation. Technical Report TUM-I0723, Technische Universität München, 2007.
• Clemens Ballarin. Algebraic structures in Axiom and Isabelle: attempt at a comparison. In J. Carette and F. Wiedijk, Programming Languages for Mechanized Mathematics (PLMMS): Hagenberg, Austria, RISC, Linz, 2007.
  
• Clemens Ballarin. Interpretation of Locales in Isabelle: Managing Dependencies between Locales. Technical Report TUM-I0607, Technische Universität München, 2006.
  
• Jesús Aransay, Clemens Ballarin and Julio Rubio. Towards a higher reasoning level in formalized Homological Algebra. In Thérèse Hardin and Renaud Rioboo, 11th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning (Calculemus), Rome, Italy; pages 84-88, Aracne Editrice S.R.L., Rome, 2003.
• Jesús Aransay, Clemens Ballarin and Julio Rubio. Deduction and Computation in Algebraic Topology. In J. A. Alonso et al., First Ibero-American Workshop on Automated Deduction and Artificial Intelligence (IDEIA): Sevilla, Spain; pages 47-54, 2002.
• Clemens Ballarin and Manuel Kauers. Solving Parametric Linear Systems: an Experiment with Constraint Algebraic Programming. In Heinz Kredel and Wolfgang K. Seiler, Eighth Rhine Workshop on Computer Algebra: Mannheim, Germany; pages 101-114, 2002. Superseded by SIGSAM Bulletin publication above.
• A challenge for sound integration of computer algebra. Calculemus and Types workshop, Eindhoven, The Netherlands, July 1998. Available as dvi.

My PhD thesis

• Computer Algebra and Theorem Proving. Available as University of Cambridge, Computer Laboratory Technical Report number 473, 1999. Available: abstract, postscript