 | 2010 |
|---|
| 12 |       | Jesús Aransay,
Clemens Ballarin,
Julio Rubio:
Generating certified code from formal proofs: a case study in homological algebra.
Formal Asp. Comput. 22(2): 193-213 (2010) |
| 2008 |
|---|
| 11 | | Jesús Aransay,
Clemens Ballarin,
Julio Rubio:
A Mechanized Proof of the Basic Perturbation Lemma.
J. Autom. Reasoning 40(4): 271-292 (2008) |
| 2006 |
|---|
| 10 | | Clemens Ballarin:
Interpretation of Locales in Isabelle: Theories and Proof Contexts.
MKM 2006: 31-43 |
| 2005 |
|---|
| 9 | | Jesús Aransay,
Clemens Ballarin,
Julio Rubio:
Extracting Computer Algebra Programs from Statements.
EUROCAST 2005: 159-168 |
| 8 | | Clemens Ballarin:
Fast Fourier Transform.
Archive of Formal Proofs 2005: (2005) |
| 7 | | Alessandro Armando,
Clemens Ballarin:
A reconstruction and extension of Maple's assume facility via constraint contextual rewriting.
J. Symb. Comput. 39(5): 503-521 (2005) |
| 2004 |
|---|
| 6 | | Jesús Aransay,
Clemens Ballarin,
Julio Rubio:
Four Approaches to Automated Reasoning with Differential Algebraic Structures.
AISC 2004: 222-235 |
| 2003 |
|---|
| 5 | | Clemens Ballarin:
Locales and Locale Expressions in Isabelle/Isar.
TYPES 2003: 34-50 |
| 2001 |
|---|
| 4 | | Alessandro Armando,
Clemens Ballarin:
Maple's evaluation process as constraint contextual rewriting.
ISSAC 2001: 32-37 |
| 1999 |
|---|
| 3 | | Clemens Ballarin,
Lawrence C. Paulson:
A Pragmatic Approach to Extending Provers by Computer Algebra - with Applications to Coding Theory.
Fundam. Inform. 39(1-2): 1-20 (1999) |
| 1998 |
|---|
| 2 | | Clemens Ballarin,
Lawrence C. Paulson:
Reasoning About Coding Theory: The Benefits We Get from Computer Algebra.
AISC 1998: 55-66 |
| 1995 |
|---|
| 1 | | Clemens Ballarin,
Karsten Homann,
Jacques Calmet:
Theorems and Algorithms: An Interface between Isabelle and Maple.
ISSAC 1995: 150-157 |
Data released under the ODC-BY 1.0 license — See also our legal information page