coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Bas Spitters <spitters AT cs.ru.nl>
To: Andreas Schropp <schropp AT in.tum.de>
Cc: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>, Coq Club <coq-club AT inria.fr>, Andrei Popescu <uuomul AT yahoo.com>
Subject: Re: [Coq-Club] Inductive data types modulo equations in Coq
Date: Tue, 14 May 2013 11:28:24 +0200

On Mon, May 6, 2013 at 9:16 PM, Andreas Schropp <schropp AT in.tum.de> wrote:

Alternatively I would like to name the (future) implementors of
this Coq extension and not just point to the homotopy blog.

Perhaps, this paper is currently the best write-up of what a feature implementation could look like:
https://www.cs.cmu.edu/~drl/pubs/lh112tt/lh122tt-final.pdf

[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, Pierre Courtieu, 05/15/2013
    - Re: [Coq-Club] Inductive data types modulo equations in Coq, Bas Spitters, 05/14/2013
  - Re: [Coq-Club] Inductive data types modulo equations in Coq, Bas Spitters, 05/14/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