17th Symposium on the Integration of
Symbolic Computation and Mechanised Reasoning

Calculemus 2010

Paris, France    6th-7th July 2010


Conference Programme

Tuesday, July 6th 2010

Welcome (15:20-15:30)

Session 1 (15:30-16:30, Chair: James H. Davenport) (Regular Papers)

15:30-16:00 Reducing Expression Size using Rule-Based 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:00-16: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:30-17:00)

Session 2 (17:00-18:30, Chair: Andrea Asperti) (Regular Papers)

17:00-17: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:30-18: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 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.

18:00-18: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 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.

Calculemus Business Meeting (18:45-19:30)

Wednesday, July 7th 2010

Calculemus Invited Talk (8:30-9:30)

8:30-9: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 mid-eighties. 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:30-10:30, Chair: Jacques Carette) (Regular Papers)

09:30-10: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:00-10: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 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.

Coffee Break (10:30-11:00)

Session 4 (11:00-11:40, Chair: Volker Sorge) (Emerging Trends Papers)

11:00-11:20 What are the rules of ``elementary algebra''?
James Davenport and Chris Sangwin

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.

11:20-11:40 Interactive Documents as Interfaces to Computer Algebra Systems: JOBAD and Wolfram|Alpha
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.

Session 5 (11:40-12:20, Chair: Volker Sorge) (Demos)

11:40-12: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:00-12:20 The Focalize Environment
Renaud Rioboo

Abstract: TBA.

Closing Remarks (12:20-12:30)

Thursday, July 8th 2010

Calculemus/PLMMS Invited Talk (8:30-9:30)

8:30-9: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.