Publications of Clemens Ballarin
Refereed publications
- 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
Back to my home
page.
Copyright © 2002 - 2008 by Clemens Ballarin
Last updated 28 April 2008.