Abstract: This paper describes continuing progress on the development of a repository of transformation rules relevant to indefinite integration. The methodology, however, is not restricted to integration. Several optimization goals are being pursued, including achieving the best form for the output, reducing the size of the repository while retaining its scope, and minimizing the number of steps required for the evaluation process. New optimizations for expression size are presented.

Abstract: Decomposing the domain of a function into parts has many uses in mathematics. A domain may naturally be a union of pieces, a function may be defined by cases, or different boundary conditions may hold on different regions. For any particular problem the domain can be given explicitly, but when dealing with a family of problems given in terms of symbolic parameters, matters become more difficult. This article shows how hybrid sets, that is multisets allowing negative multiplicity, may be used to express symbolic domain decompositions in an efficient, elegant and uniform way, simplifying both computation and reasoning. We apply this theory to the arithmetic of piecewise functions and symbolic matrices and show how certain operations may be reduced from exponential to linear complexity.

Abstract: We prove formally that the first order theory of algebraically closed fields enjoys quantifier elimination, and hence is decidable. This proof is organized in two modular parts. We first reify the first order theory of rings and prove that quantifier elimination leads to decidability. Then we implement an algorithm which constructs a quantifier free formula from any first order formula in the theory of ring. If the underlying ring is in fact an algebraically closed field, we prove that the two formulas have the same semantic. The algorithm producing the quantifier free formula is programmed in continuation passing style, which leads to both a concise program and an elegant proof of semantic correctness.

Abstract: We propose a formal study of interval analysis that concentrates on theoretical aspects rather than on computational ones. In particular we are interested in conditions for regularity of interval matrices. An interval matrix is called regular if all scalar matrices included in the interval matrix have non-null determinant and it is called singular otherwise. Regularity plays a central role in solving systems of linear interval equations. Several tests for regularity are available and widely used, but sometimes rely on rather involved results, hence the interest in formally verifying such conditions of regularity. In this paper we set the basis for this work: we define intervals, interval matrices and operations on them in the proof assistant Coq, and verify criteria for regularity and singularity of interval matrices.

Abstract: The main goal of our work is to formally prove the correctness of the key commands of the SCHUR software, an interactive program for calculating with characters of Lie groups and symmetric functions. The core of the computations relies on enumeration and manipulation of combinatorial structures. As a first "proof of concept", we present a formal proof of the conjugate function, written in C. This function computes the conjugate of an integer partition. To formally prove this program, we use the Frama-C software. It allows us to annotate C functions and to generate proof obligations, which are proved using several automated theorem provers. In this paper, we also draw on methodology, discussing on how to formally prove this kind of program.

Abstract: Computational content encoded into constructive type theory proofs can be used to make computing experiments over concrete data structures. In this paper, we explore this possibility when working in Coq with chain complexes of infinite type (that is to say, generated by infinite sets) as a part of the formalization of a hierarchy of homological algebra structures.

Abstract: We provide a ``shared axiomatization'' of natural numbers and hereditarily finite sets built around a polymorphic abstraction of bijective base-2 arithmetics. The ``axiomatization'' is described as a progressive refinement of Haskell type classes with examples of instances converging to an efficient implementation in terms of arbitrary length integers and bit operations. As an instance, we derive algorithms to perform arithmetic operations efficiently directly with hereditarily finite sets. The self-contained source code of the paper is available at http://logic.cse.unt.edu/tarau/research/2010/unified.hs.

Abstract: Many systems dealing with mathematics, including but not limited to computer-aided assessment (CAA) software, have to deal with "equality up to the usual rules of algebra", but what this phrase means is often less clear. Even when they are clear in abstract, implementing them in a computer algebra system, which has to deal with the mathematics users have typed, complete with complications such as division (rather than multiplication by the inverse), binary subtraction etc., is far from clear. In this paper, we outline some pitfalls, and what we have learned about solving these problems.

Abstract: Interactivity and customization are common trends guiding the design of services on the web. Not only can users adapt content to their preferences, they can also dynamically aggregate content from various sources on interactive pages in their browser that thus turn into powerful command centers (e. g. iGoogle). Our JOBAD architecture embeds mathematical services into XHTML+MathML documents. JOBAD is a modular JavaScript framework for interactive services such as term folding or definition lookup.
We have now enhanced it with a client for computer algebra. It lets the user select mathematical expressions and ask a CAS to compute, graph, or rewrite them. We have done first steps towards an integration with the WolframjAlpha web service API, which gives access to Mathematica as well as a large mathematical knowledge base. We are currently working on a generalization towards arbitrary CAS backends and thus promoting documents as interfaces to computer algebra systems.

Abstract: A relatively small number of universal data types are used as basic building blocks in programming languages corresponding to a few well tested mathematical abstractions. The demo, based on the Mathematica notebook at http://logic.cse.unt.edu/tarau/research/2010/iso.nb visualizes equivalences between sequences, sets, trees representing hereditarily finite sets and functions, recursive applications of unpairing functions as well as various types of graphs. As an application, a few examples of symbolic arithmetic computations described in my CALCULEMUS 2010 paper, based on the Haskell code at http://logic.csci.unt.edu/tarau/research/2010/unified.hs, follows.

Abstract: TBA.