CaCoS 2012
CaCoS will be held on Thursday July 26, 2012, in Grenoble, France.
CaCoS  Categorical Computer Science
is a Satellite Workshop of
ISSAC 2012
 International Symposium on Symbolic and Algebraic Computation.
All categorical methods in computer science are welcome at the CaCoS workshop.
An aim of the CaCoS 2012 workshop is to focus on the use of proof assistants
for computer science and computer algebra.
Location
On the campus of the University of Grenoble.
UFR im2ag  Batiment F  Amphithéatre F022  60, rue de la Chimie 
38042 Saint Martin d'Hères:
Access.
PROGRAM:

08:4509:00 
welcome

09:0009:45  Loïc Pottier (INRIA Sophia):
An example of automation in Coq using types classes and reflection

09:4510:30  Assia Mahboubi (INRIA, LIX):
Toward a formal proof that zeta(3) is irrational

10:3011:00  coffee break

11:0011:45  PaulAndré Melliès (CNRS, PPS):
A short tutorial on combinatorial species and analytic functors

11:4512:30  Barbara Petit (Univ. of Bologna):
Categorical Semantics of the Lambda Calculus with Constructors

12:3014:15  lunch

14:1515:00  Guillaume Melquiond (INRIA, LRI):
Wave Equation Numerical Resolution:
a Comprehensive Mechanized Proof of a C Program

15:0015:45  Ioana Pasca (INRIA, LIP):
Formal Proofs for Taylor Models in Coq

15:4516:15  coffee break

16:1517:00  Célia Picard (IRIT):
Coinductive Graph Representation

17:0017:45  Damien Pous (CNRS, ENSL):
Bisimulations up to for finite automata (Joint work with Filippo Bonchi)
ABSTRACTS:

Loïc Pottier:
An example of automation in Coq using types classes and reflection
We will present a tactic in Coq which proves polynomial identity,
using reflection, type classes, and Buchberger algorithm.
We will show examples of this tactic applied to automatic geometric theorem
proving.

Assia Mahboubi:
Toward a formal proof that zeta(3) is irrational
In 1978, R. Apéry claimed that he had proved the
irrationality of zeta(3). The
status of this result remained controversial for a couple of months
before being validated by the careful proofreading of his
collegues (see "A proof that Euler missed...", A. Van
der Poorten, 1978). A striking feature of this proof is that it
involves only rather elementary arguments, combining the
properties of auxiliary sequences that seem to come out of thin
air. It remains unclear that some general method can be
extracted from this proof in order to obtain similar results for other
constants, like other values of the zeta function. However
part of the study led by A. Apéry can be automatized by a generic method
for the study of hypergeormetric identities based on socalled creative
telescoping. In particular, this method can be implemented as an
oracle which produces recurrence relations satisfied by a given
series and which validates its result by a certificate. In this talk, we
describe the ongoing formalization of the irrationality of zeta(3) in
the Coq proof assistant, using the Maple computer algebra system as an
external oracle. This is a joint work with Frédéric Chyzak
(Inria) and Thomas SibutPinote (ENS Lyon).

PaulAndré Melliès:
A short tutorial on combinatorial species and analytic functors.
Cancelled.

Barbara Petit:
Categorical Semantics of the Lambda Calculus with Constructors
The lambda calculus with constructors decomposes the pattern matching
"à la ML" into a simple analysis on constants and some commutation rules.
This leads to a quite unusual computing design, but the presence of such
atomic rules helps to define a categorical model for the calculus.
We give a notion of categorical model for the lambda calculus with
constructors, that is complete for the calculus without match failure
(which can be proven thanks to the PER category). Then we show how to
instantiate this model in non syntactic categories, using CPS techniques.

Guillaume Melquiond:
Wave Equation Numerical Resolution:
a Comprehensive Mechanized Proof of a C Program
We have formally proved correct a C program that implements a numerical
scheme for the resolution of the onedimensional acoustic wave equation.
Such an implementation introduces errors at several levels: the
numerical scheme introduces method errors, and floatingpoint
computations lead to roundoff errors. We have annotated this C program
to specify both method error and roundoff error. We have used FramaC
to generate theorems that guarantee the soundness of the code. We have
discharged these theorems using SMT solvers, Gappa, and Coq. This
involves a large Coq development to prove the adequacy of the C program
to the numerical scheme and to bound errors. To our knowledge, this is
the first time such a numerical analysis program is fully
machinechecked.

Ioana Pasca:
Formal Proofs for Taylor Models in Coq
One of the most common and practical ways of representing
a real function on machines is by using a polynomial approximation. It
is then important to properly handle the error introduced by such an
approximation. The purpose of this work is to offer guaranteed error
bounds for a specific kind of rigorous polynomial approximation called
Taylor model. We carry out this work in the Coq proof assistant, with a
special focus on genericity and efficiency for our implementation. We give
an abstract interface for rigorous polynomial approximations,
and we instantiate this interface to the case of Taylor models with interval
coefficients, while providing all the machinery for computing them.
We compare the performances of our implementation in Coq with those
of the Sollya tool, which contains an implementation of Taylor models in C.
We prove correct our implementation of Taylor models with respect
to the axiomatic formalization of real functions available in Coq's
standard library.

Célia Picard:
Coinductive Graph Representation
This presentation stands at the interface between Model Driven Engineering
(MDE) and type theory. We aim at certifying model representation and
transformation, using the interactive theorem prover Coq for certification
matters. This talk only deals with representation and manipulation of graphs
using coinductive types. First we present our coinductive representation
of graphs. The use of coinductive types allows, among other things,
to ensure navigability by construction. While defining this representation,
we have to overcome Coq's guardedness condition using a noninductive type
to represent lists. We also define various tools to manipulate those lists
and graphs, among which the canonical relation on graphs. Then, we define
a wider (parameterized) relation on graphs. This new relation is close to
the notion of equivalence on the classical representation of graphs (set of
nodes/set of edges), but keeps the advantages offered by coinduction. Indeed,
our definition of graph induces an implicit order (both horizontally and
vertically) between the nodes. The new relation allows us to abstract from
this order. We also show that this relation is equivalent to another one
based on finite observations of graphs, which requires a nonconstructive
principle to be added to Coq's logic.

Damien Pous:
Bisimulations up to for finite automata (Joint work with Filippo Bonchi)
We introduce bisimulation up to congruence as a technique for proving
language equivalence of nondeterministic finite automata. Exploiting
this technique, we devise an optimisation of the classical algorithm
by Hopcroft and Karp that, instead of computing the whole determinised
automata, explores only a small portion of it. We then show that this
algorithm actually generalises the recently introduced ``antichain''
algorithms. We finally explain how these ideas can be presented in a
more general coalgebraic framework.
PARTICIPANTS:
 Casperson David (University of Northern British Columbia)
 Dumas JeanGuillaume (Université de Grenoble  LJK)
 Duval Dominique (Université de Grenoble  LJK)
 Echahed Rachid (CNRS  Université de Grenoble  LJK)
 Guillon Arthur (Université de Paris 7)
 Mahboubi Assia (INRIA)
 Melliès PaulAndré (CNRS  Université de Paris Diderot)
 Melquiond Guillaume (INRIA  LRI)
 Monniaux David (CNRS  VERIMAG)
 Pasca Ioana (ENS Lyon  LIP)
 Peltier Nicolas (CNRS  LIG)
 Petit Barbara (Universita di Bologna  Inria)
 Picard Celia (IRIT  Université de Toulouse)
 Pottier Loïc (INRIA)
 Pous Damien (CNRS  ENS Lyon)
 Prost Frédéric (Université de Grenoble  LIG)
 Rieg Lionel (ENS Lyon)
Registration
Please fill in the following form to register to the workshop: no
registration fee is due, but we need to know how many lunches to
provide.
Organizers:
Dominique Duval
(LJK, University of Grenoble, France)
Damien Pous
(CNRS, ENS Lyon, France)
CaCoS 2012 is sponsored by:
LJK,
ANR HPAC,
ANR CLIMT.