CaCoS 2012

PROGRAM:

• 08:45-09:00 - welcome
• 09:00-09:45 - Loïc Pottier (INRIA Sophia): An example of automation in Coq using types classes and reflection
• 09:45-10:30 - Assia Mahboubi (INRIA, LIX): Toward a formal proof that zeta(3) is irrational
• 10:30-11:00 - coffee break
• 11:00-11:45 - Paul-André Melliès (CNRS, PPS): A short tutorial on combinatorial species and analytic functors
• 11:45-12:30 - Barbara Petit (Univ. of Bologna): Categorical Semantics of the Lambda Calculus with Constructors
• 12:30-14:15 - lunch
• 14:15-15:00 - Guillaume Melquiond (INRIA, LRI): Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program
• 15:00-15:45 - Ioana Pasca (INRIA, LIP): Formal Proofs for Taylor Models in Coq
• 15:45-16:15 - coffee break
• 16:15-17:00 - Célia Picard (IRIT): Coinductive Graph Representation
• 17:00-17: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 proof-reading 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 so-called 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 Sibut-Pinote (ENS Lyon).
• Paul-André 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 one-dimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and floating-point computations lead to round-off errors. We have annotated this C program to specify both method error and round-off error. We have used Frama-C 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 machine-checked.
• 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 non-inductive 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 non-constructive 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 non-deterministic 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 Jean-Guillaume (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 Paul-André (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)

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.

Last Name: 
First Name: 
Email Address: 
Affiliation:  

Organizers:
Dominique Duval (LJK, University of Grenoble, France)
Damien Pous (CNRS, ENS Lyon, France)

CaCoS 2012 is sponsored by: LJK, ANR HPAC, ANR CLIMT.