The list of accepted papers below is ordered alphabetically by first author surname.

Links to preprints (on http://ArXiv.org) and to the final published articles (on http://www.springerlink.com) will be added as they become available.

The full proceedings of the conference are available from Springer (LNAI 6167). You can find information about it at http://www.springeronline.com/978-3-642-14127-0 or access the online version at http://www.springerlink.com/content/978-3-642-14127-0/

• 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.
  [Preprint]      [Springerlink]
• 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.
  [Preprint]      [Springerlink]
• 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.
  [Preprint]      [Springerlink]
• 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.
  [Preprint]      [Springerlink]
• 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.
  [Preprint]      [Springerlink]
• 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.
  [Preprint]      [Springerlink]
• 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.
  [Preprint]      [Springerlink]