

17th Symposium on the
Integration of
Symbolic Computation and Mechanised Reasoning
Calculemus 2010
Paris, France 6th7th July 2010



Conference Programme
Tuesday, July 6th 2010 
Welcome (15:2015:30)

Session 1 (15:3016:30, Chair: James H. Davenport) (Regular Papers)
15:3016:00 
Reducing Expression Size using RuleBased Integration
Albert Rich and David Jeffrey
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.

16:0016:30 
Symbolic Domain Decomposition
Jacques Carette, Alan Sexton, Volker Sorge and Stephen Watt
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.


Coffee Break (16:3017:00)

Session 2 (17:0018:30, Chair: Andrea Asperti) (Regular Papers)
17:0017:30 
A Formal Quantifier Elimination for Algebraically Closed Fields
Cyril Cohen and Assia Mahboubi
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.

17:3018:00 
Formally Verified Conditions for Regularity of Interval Matrices
Ioana Pasca
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 nonnull 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.

18:0018:30 
Formal Proof of SCHUR Conjugate Function
Franck Butelle, Florent Hivert, Micaela Mayero and Frédéric Toumazet
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 FramaC
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.


Calculemus Business Meeting (18:4519:30)

Wednesday, July 7th 2010 
Calculemus Invited Talk (8:309:30)
8:309:30 
Some Considerations on the Usability of Interactive Provers
Andrea Asperti
Abstract:
In spite of the remarkable achievements recently obtained in the field of
mechanization of formal reasoning, the overall usability of interactive provers
does not seem to be sensibly improved since the advent of the "second
generation" of systems, in the mideighties. We try to analyze the reasons of
such a slow progress, pointing out the main problems and suggesting some
possible research directions.


Session 3 (09:3010:30, Chair: Jacques Carette) (Regular Papers)
09:3010:00 
Computing in Coq with Infinite Algebraic Data Structures
Cesar Dominguez and Julio Rubio
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.

10:0010:30 
A Unified Formal Description of Arithmetic and Set Theoretical Data Types
Paul Tarau
Abstract:
We provide a ``shared axiomatization'' of natural numbers and hereditarily
finite sets built around a polymorphic abstraction of bijective base2
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 selfcontained source code of the
paper is available at http://logic.cse.unt.edu/tarau/research/2010/unified.hs.


Coffee Break (10:3011:00)

Session 4 (11:0011:40, Chair: Volker Sorge)
(Emerging Trends Papers)
11:0011:20 
What are the rules of ``elementary algebra''?
James Davenport and Chris Sangwin
Abstract:
Many systems dealing with mathematics, including but not limited to
computeraided 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.
[Preprint]
[CEDRIC link]

11:2011:40 
Interactive Documents as Interfaces to Computer Algebra Systems: JOBAD and WolframAlpha
Catalin David, Christoph Lange and Florian Rabe
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.
[Preprint]
[CEDRIC link]


Session 5 (11:4012:20, Chair: Volker Sorge) (Demos)
11:4012:00 
Visualizing Data Type Isomorphims
Paul Tarau
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.

12:0012:20 
The Focalize Environment
Renaud Rioboo
Abstract:
TBA.


Closing Remarks (12:2012:30)

Thursday, July 8th 2010 
Calculemus/PLMMS Invited Talk (8:309:30)
8:309:30 
Mechanized Mathematics
Jacques Carette
Abstract:
If one were designing an entirely new mathematical assistant, what might it
look like? Problems and some favoured solutions are presented.



