Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page