coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] A fast "eq" predicate for Gallina?

From: Jean-Christophe Léchenet <jean-christophe.lechenet AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] A fast "eq" predicate for Gallina?
Date: Thu, 21 Jan 2021 11:18:28 +0100

Oh - bright shiny link to useful paper!;-)

Another interesting pointer is Jacques-Henri Jourdan's PhD thesis: https://jhjourdan.mketjh.fr/thesis_jhjourdan.pdf.
See Section 9.1, Safe Physical Equality in Coq: the physEq Approach.

Jean-Christophe

[Coq-Club] A fast "eq" predicate for Gallina?, jonikelee AT gmail.com, 01/20/2021
- Re: [Coq-Club] A fast "eq" predicate for Gallina?, Sylvain Boulmé, 01/20/2021
  - Re: [Coq-Club] A fast "eq" predicate for Gallina?, jonikelee AT gmail.com, 01/20/2021
    - Re: [Coq-Club] A fast "eq" predicate for Gallina?, Jean-Christophe Léchenet, 01/21/2021
- Re: [Coq-Club] A fast "eq" predicate for Gallina?, Adam Chlipala, 01/20/2021
  - Re: [Coq-Club] A fast "eq" predicate for Gallina?, Sylvain Boulmé, 01/20/2021
  - Re: [Coq-Club] A fast "eq" predicate for Gallina?, jonikelee AT gmail.com, 01/20/2021
    - Re: [Coq-Club] A fast "eq" predicate for Gallina?, Pierre-Marie Pédrot, 01/20/2021
      - Re: [Coq-Club] A fast "eq" predicate for Gallina?, jonikelee AT gmail.com, 01/20/2021
        
        Re: [Coq-Club] A fast "eq" predicate for Gallina?, Xavier Leroy, 01/21/2021
        
        Re: [Coq-Club] A fast "eq" predicate for Gallina?, jonikelee AT gmail.com, 01/21/2021
  - Re: [Coq-Club] A fast "eq" predicate for Gallina?, Pierre-Marie Pédrot, 01/20/2021
    - Re: [Coq-Club] A fast "eq" predicate for Gallina?, Adam Chlipala, 01/20/2021
    - Re: [Coq-Club] A fast "eq" predicate for Gallina?, Mario Carneiro, 01/20/2021