coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Issues/questions with extraction.

From: Andrej Bauer <andrej.bauer AT andrej.com>
To: coq-club <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] Issues/questions with extraction.
Date: Fri, 5 Jun 2009 16:00:29 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

I have always wondered about the mathematical background behind
extraction, and it seems like a good opportunity to ask. Is there a
place where I could read about the mathematical theory that supports
Coq's extraction mechanisms? I suppose it's a kind of realizability
interpretation of Coq's language, right?

Andrej

[Coq-Club] Issues/questions with extraction., Adam Koprowski
- Re: [Coq-Club] Issues/questions with extraction., Pierre Letouzey
  - Re: [Coq-Club] Issues/questions with extraction., St�phane Lescuyer
  - Re: [Coq-Club] Issues/questions with extraction., Adam Koprowski
    - Re: [Coq-Club] Issues/questions with extraction., Yves Bertot
      - Re: [Coq-Club] Issues/questions with extraction., Andrej Bauer
        
        Re: [Coq-Club] Issues/questions with extraction., Adam Chlipala
        
        Re: [Coq-Club] Issues/questions with extraction., Jean-Francois Monin
        
        Re: [Coq-Club] Issues/questions with extraction., Ryan Rusich