coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Inductive data types modulo equations in Coq

From: Andreas Schropp <schropp AT in.tum.de>
To: Frederic Blanqui <frederic.blanqui AT inria.fr>
Cc: coq-club AT inria.fr, Andrei Popescu <uuomul AT yahoo.com>
Subject: Re: [Coq-Club] Inductive data types modulo equations in Coq
Date: Mon, 06 May 2013 21:19:02 +0200

On 05/06/2013 11:52 AM, Frederic Blanqui wrote:

Hello.

With Pierre Weis and Richard Bonichon, I develop a tool called Moca (see http://moca.inria.fr/), for generating construction functions (in OCaml currently) for types modulo some equations like in your example [1]. We also started to prove in Coq the generated functions for the following equational theories: monoids, groups and abelian groups. You can find the corresponding Coq files in the Moca sources.

Best regards,

Frederic.

[1] On the implementation of construction functions for non-free concrete data types. F. Blanqui, T. Hardin and P. Weis. ESOP'07.

Thanks, I will look into that.

Cheers,
Andy

[Coq-Club] Inductive data types modulo equations in Coq, Andreas Schropp, 05/05/2013
- Re: [Coq-Club] Inductive data types modulo equations in Coq, Arnaud Spiwack, 05/06/2013
  - Re: [Coq-Club] Inductive data types modulo equations in Coq, Andreas Schropp, 05/06/2013
    - Re: [Coq-Club] Inductive data types modulo equations in Coq, Arnaud Spiwack, 05/07/2013
      - Re: [Coq-Club] Inductive data types modulo equations in Coq, Frederic Blanqui, 05/07/2013
- Re: [Coq-Club] Inductive data types modulo equations in Coq, Frederic Blanqui, 05/06/2013
  - Re: [Coq-Club] Inductive data types modulo equations in Coq, Andreas Schropp, 05/06/2013