Publications of Clemens Ballarin

Book Contributions

• Clemens Ballarin. Tutorial to locales and locale interpretation. In Contribuciones Científicas en honor de Mirian Andrés, pages 123–140. Servicio de Publicaciones de la Universidad de La Rioja, Logroño, Spain, 2010.

Journal Articles

• Clemens Ballarin. Exploring the Structure of an Algebra Text with Locales. Journal of Automated Reasoning, 64(6):1093–1121, 2020. © Springer (Publisher's Version)
• Clemens Ballarin. Locales: a module system for mathematical theories. Journal of Automated Reasoning, 52(2):123–153, 2014. © Springer (Publisher's Version)
• Jesús Aransay, Clemens Ballarin and Julio Rubio. Generating certified code from formal proofs: a case study in homological algebra. Formal Aspects of Computing, 22(2):193–213, 2010.
• 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. © 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.
• 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 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.

Conference Articles

• Clemens Ballarin. Two Generalisations of Roşu and Chen's Trace Slicing Algorithm A. In B. Bonakdarpour and S.A. Smolka, RV 2014, LNCS 8734, pages 15–30, 2014. © Springer (Publisher's Version).
• 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.
• 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. 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. 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 and Abstracts

• Clemens Ballarin. An Antiquotation for Locale Graphs. Isabelle workshop, June 2020.
• Clemens Ballarin. Towards Monitoring Temporal Properties with JamaicaVM. In Proceedings of the 11th International Workshop on Java Technologies for Real-time and Embedded Systems (JTRES '13), Karlsruhe, Germany, pages 89-95, 2013. © ACM (Publisher's Version).
• Clemens Ballarin. Reading an Algebra Textbook. In C. Lange et al., MathUI, OpenMath, PLMMS and ThEdu Workshops and Work in Progress at the Conference on Intelligent Computer Mathematics, Bath, UK, CEUR Workshop Proceedings 1010, 2013.
  
• 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