coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Kevin Sullivan <sullivan.kevinj AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] A CS1 course inspired by Pierce's SF.
Date: Tue, 1 Nov 2016 14:34:30 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=sullivan.kevinj AT gmail.com; spf=Pass smtp.mailfrom=sullivan.kevinj AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f48.google.com
Ironport-phdr: 9a23:eO2g/Rd5PE7hAisbJpr5dOiSlGMj4u6mDksu8pMizoh2WeGdxc29bR7h7PlgxGXEQZ/co6odzbGH6eawACdZuM/J8ChbNscTB1ld0YRetjdjKfDGIHWzFOTtYS0+EZYKf35e1Fb/D3JoHt3jbUbZuHy44G1aMBz+MQ1oOra9QdaK3Izkn9y1rpbUekBDgCe3SbJ0NhS/6wvL5ecMho43Casvyx2BmWZMf+VIzGUgcUmOmxL9+M62up1u7SVWudou8sdBVePxeKFuHu8QNygvL21gvJ6jjhLEVwbavnY=

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

[Coq-Club] A CS1 course inspired by Pierce's SF., Kevin Sullivan, 11/01/2016
- Re: [Coq-Club] A CS1 course inspired by Pierce's SF., Théo Zimmermann, 11/02/2016
  - Re: [Coq-Club] A CS1 course inspired by Pierce's SF., Kevin Sullivan, 11/02/2016
    - Re: [Coq-Club] A CS1 course inspired by Pierce's SF., Kevin Sullivan, 11/05/2016