coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Interest in Coq-based mathematics classes?

From: "Edward Z. Yang" <ezyang AT MIT.EDU>
To: Kristopher Micinski <krismicinski AT gmail.com>
Cc: Andrej Bauer <andrej.bauer AT andrej.com>, Coq Club <coq-club AT inria.fr>, Adam Chlipala <adamc AT csail.mit.edu>
Subject: Re: [Coq-Club] Interest in Coq-based mathematics classes?
Date: Tue, 18 Sep 2012 00:05:50 +0200

Excerpts from Kristopher Micinski's message of Mon Sep 17 23:38:37 +0200 2012:
> You are aware that the university of Pennsylvania teaches a course using
> the software foundations textbook which slightly satisfies this idea? It's
> the closest thing I can think of off the top of my head. I believe Pierce
> has a talk on it, lambda the ultimate ta.

Software Foundations is a great textbook, but it focuses on aspects of
mathematics and programming languages theory which traditionally theorem
provers like Coq have been quite strong at. I believe Adam is interested
in targeted mathematics that goes beyond the simple structural induction
we know and love.

Edward

[Coq-Club] Interest in Coq-based mathematics classes?, Adam Chlipala, 09/17/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, immanuel litzroth, 09/17/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Andrej Bauer, 09/17/2012
  - Re: [Coq-Club] Interest in Coq-based mathematics classes?, Kristopher Micinski, 09/17/2012
    - Re: [Coq-Club] Interest in Coq-based mathematics classes?, Edward Z. Yang, 09/18/2012
      - Re: [Coq-Club] Interest in Coq-based mathematics classes?, Pierce Benjamin C., 09/18/2012
        
        Re: [Coq-Club] Interest in Coq-based mathematics classes?, Kristopher Micinski, 09/18/2012
        
        Re: [Coq-Club] Interest in Coq-based mathematics classes?, Adam Chlipala, 09/18/2012
        
        Re: [Coq-Club] Interest in Coq-based mathematics classes?, Kristopher Micinski, 09/18/2012
        Re: [Coq-Club] Interest in Coq-based mathematics classes?, Benjamin C. Pierce, 09/18/2012
    - Re: [Coq-Club] Interest in Coq-based mathematics classes?, Benjamin Werner, 09/18/2012
      - Re: [Coq-Club] Interest in Coq-based mathematics classes?, Pierre Courtieu, 09/18/2012
      - Re: [Coq-Club] Interest in Coq-based mathematics classes?, Adam Chlipala, 09/19/2012
  - Re: [Coq-Club] Interest in Coq-based mathematics classes?, Adam Chlipala, 09/19/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Jonas Oberhauser, 09/20/2012