Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] A CS1 course inspired by Pierce's SF.

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] A CS1 course inspired by Pierce's SF.


Chronological Thread 
  • From: Théo Zimmermann <theo.zimmi AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] A CS1 course inspired by Pierce's SF.
  • Date: Wed, 02 Nov 2016 08:28:59 +0000
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f45.google.com
  • Ironport-phdr: 9a23:HC3uEBLqXSfASi9DQNmcpTZWNBhigK39O0sv0rFitYgXLfnxwZ3uMQTl6Ol3ixeRBMOAuqgC27Cd6vm/ESxYuNDa7yBEKMQNHzY+yuwo3CUYSPafDkP6KPO4JwcbJ+9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEtfre9ScbuiJG80Pn38JnOaS1JgiC8aPV8NkaYtwLU4/UWAIxVGKc0zxbTp3JOfawC2WNlIhSBnhP55++/+Zdi92JbvPd3pJ0IarnzY6ltFe8QNz8hKW1gvMA=
Hello,

A README or some installation instructions could be useful there. I would be interested but I can't spend too much time trying to understand where to start. I have had a look at Idris some time ago: read the tutorial almost entirely and then was bored, without a real project to practice on, so your course could be a good path to have a second look.

Cheers,
Théo

Le mar. 1 nov. 2016 à 19:35, Kevin Sullivan <sullivan.kevinj AT gmail.com> a écrit :

A few of you might be interested in the materials I've been developing with my CS1 class of about 100 first-semester students in our College of Arts and Sciences. You can go back through tagged versions to see the progression. I teach the course using Idris, which I decided is better than Coq for this particular application. We cover most of the FP stuff, and more, but not proof engineering. That said, this course lines up students to move into SF directly

https://github.com/kevinsullivan/cs1113f16


Archive powered by MHonArc 2.6.18.

Top of Page