The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

I have added a README. The most important point for making sense of the repo is that it's a sequence of tagged versions of the prelude library that we've taken two months, in class, to build, starting with unit and bool and proceeding through state, _expression_, command, and an operational semantics (eval) for expressions and commands. For the rest of the semester (about a month) we'll develop and use our little Imp language in Idris to open a window on imperative programming in Python. The idea is that once they get over the hump of understanding the state-transformation model of imperative programming, they will already have good intuition for all of the major data types built into Python, from bool and arithmetic through lists, dictionaries, tuples, and all the rest.

If one ever wanted to give this course a try, a good approach would be (1) clone my repo, (2) check out each minor version in turn, (3) and then show the students, in class, with all their laptops open, how to get through the construction of that step. Every class is programming. We're building everything together at all times.

https://github.com/kevinsullivan/cs1113f16

Kevin

On Wed, Nov 2, 2016 at 8:22 AM, Kevin Sullivan <sullivan.kevinj AT gmail.com> wrote:

Will do. Agreed. --Kevin

On Wed, Nov 2, 2016 at 4:28 AM, Théo Zimmermann <theo.zimmi AT gmail.com> wrote:

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