WIP Syllabus

[marco-vassena]

I have added a tentative syllabus following pretty much Software Foundations.

Remember that everyone has to present a topic (an interactive COQ session with the highlights of the chapter will probably do), so I invite you to pick-up yours (first-come first-served).

I have included a first session on the basics, since it turns out that not everyone in the group has prior experience with proof assistants. I encourage those who are less familiar with proofs assistants to present it, so that then we can progress uniformly.

Feel free to edit and adjust the syllabus.

[AndreasLoow]

I think basing the whole course on only SF will lead to a too basic course, given that this is supposed to be a phd student-level course. As mentioned in the irc channel, I committed some suggestions based on your syllabus. See b9223cd6a73c22423414a699805c8550ff0b47d7. I think it makes sense to follow SF, but it must be complemented with additional material. Especially towards the end of the course.

[marco-vassena]

The fact that PhD students take the course does not make it PhD level. In fact we are allowed to take master level courses for credits as well. But anyway I am in favour of adding topics that deviate from SF. Please add them in the syllabus as well so that we have a high-level view of the structure of the course.

[vlopezj]

@marco-vassena I was hoping to present inductive propositions during next meeting. If we have succeeded done exercises 1, 2, 3 we should have enough background by then.

[marco-vassena]

I personally do not mind, but there are folks that have never used a proof assistant before and might not get to that level by themselves in in such short time.

That was the purpose of having a basic lecture, so that they have more time to get on track and then be able to follow the rest of the course.

On 04 Feb 2017, at 23:15, Víctor López Juan notifications@github.com<mailto:notifications@github.com> wrote:

@marco-vassenahttps://github.com/marco-vassena I was hoping to present inductive propositions during next meeting. If we have succeeded done exercises 1, 2, 3 we should have enough background by then.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHubhttps://github.com/vlopezj/coq-course/issues/12#issuecomment-277482042, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AFN09sYyOtf_s8tJZ0jSy4KuxY1u5v9Pks5rZPh9gaJpZM4L3LBI.

[AndreasLoow]

I agree with @vlopezj here. The material covered in part 1, 2 and 3 is basically the same material as in the beginning of SF (- Poly), only in faster pace -- so, it would be pointless to have the same material twice. One can follow part 1, 2 and 3 and then complement with SF where one has problems understanding. But of course, people new to the area have to spend more time in the beginning compared to those with previous exposure.

If we cover part 1, 2 and 3 for the first (actual) meeting, and something equivalent to part 4 and 5 + some of the IndProp stuff (but with the IndProp presentation during meeting one, as a preview, I assume) for the second we have essentially the same pace as in Pierce's course. So it should be doable for complete beginners also.

But I think we should also consider of how much use a presentation based on material from SF is. The material is already so well presented there, so what would be the point of presenting it again? I think it would be more useful to base presentations on other sources, e.g. ssreflect, coq.io, how coq is used in compcert, problems when dealing with equality between different types, monads in coq, anything mentioned in "additional topics", etc.

[vlopezj]

To elaborate a bit more:

Part of the reason for waiting 2 weeks before the next session is to give beginners time to go through the material for session 1 on their own, in particular the tutorial:

Tutorial: https://coq.inria.fr/distrib/V8.6/files/Tutorial.pdf

Then they can test their understanding by attempting the exercises (exercises/ex{1,2,3}.v).

We will look at the exercises during the second half of the session, and then we can solve any questions from everyone, including beginners. I agree with what @marco-vassena said of having a beginner be the one showing their solution attempts.

If questions arise before then, one can always open an issue, or ask on the chat.

Marco Vassena notifications@github.com skrev: (5 februari 2017 10:27:36 CET)

I personally do not mind, but there are folks that have never used a proof assistant before and might not get to that level by themselves in in such short time.

That was the purpose of having a basic lecture, so that they have more time to get on track and then be able to follow the rest of the course.

On 04 Feb 2017, at 23:15, Víctor López Juan notifications@github.com<mailto:notifications@github.com> wrote:

@marco-vassenahttps://github.com/marco-vassena I was hoping to present inductive propositions during next meeting. If we have succeeded done exercises 1, 2, 3 we should have enough background by then.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHubhttps://github.com/vlopezj/coq-course/issues/12#issuecomment-277482042, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AFN09sYyOtf_s8tJZ0jSy4KuxY1u5v9Pks5rZPh9gaJpZM4L3LBI.

-- You are receiving this because you commented. Reply to this email directly or view it on GitHub: https://github.com/vlopezj/coq-course/issues/12#issuecomment-277507141

[dschoepe]

The prerequisites say:

Participants are expected to be familiar with a functional language with a rich type system, such as Agda, Haskell or Scala.

I guess that pretty much covers the content of the first exercises, so even if one hasn't used a proof system before, it should still be fairly basic.

[vlopezj]

Btw, @AndreasLoow : you seem to have a good number of ideas of additional topics we can cover. It would be great to have a list of those under the current syllabus.

[AndreasLoow]

I think most things are already mentioned in either the additional topics list or in plan.md. But more importantly, I think it should be up to each participant to find and summarize some topic that they feel is worthwhile. A list of suggestions is of course helpful in this process, but not essential.

[Airini]

I won't have enough time to prepare for presenting the next session myself, so would prefer to take my slot later on in the study period.

[AndreasLoow]

I will repeat what was said in the IRC channel:

09:22:10> hm, regarding presentations. i have an idea, maybe it would make sense to also allow shorter presentations (like only 10 minutes or so) but require two such smaller presentations. this would not have to cover a whole chapter in sf or so, but could instead be something like "i know agda since previously so here as some things i have notice that are different from coq", "i read a paper about compcert and here are a few things to note", "i read something about sharing proofs between isabelle and coq, here are some things that are interesting about that", "here are some ways you can convince the termination checker that your programs terminate", or anything. 09:22:19> or maybe 10 minutes are too short, i don't know 09:22:56> but if so, i could maybe say something about infinite data next-next time (not here next time, in cambridge then)

I added myself to the next-next session in syllabus.md, and will hopefully do something related to infinity/co-induction/blablabla then. Preparing an as well-done presentation as done by vlopezj last session is probably very time consuming, and it might be the case that for some sessions nobody has that much time.

Ping @Airini: Maybe you have time for a shorter presentation next time? Or anyone else for that matter?

[simonr89]

Since most of the material in that course is going to be provided by the presentations, I think it's reasonable to ask a little bit of commitment from the people who do those presentations. 10 minutes seems very short: what are we going to do with the rest of the 2 hours that meetings are supposed to last?

I registered myself for the next slot, I'm planning to talk about the calculus of constructions, proof terms, Prop vs Set...

[AndreasLoow]

Sure, if people can commit to such a thing that would be better. My comment was based on that it seemed difficult to find somebody to do it for the upcoming slot.

[Airini]

Excuse the lack of responses from my part. I was away and disconnected the whole of last week (the reason behind my lack of time for the slot this week).

@AndreasLoow @simonr89 I agree that one should commit to do more than 10 minutes. Splitting a session in, say, two presentations + time for discussion could be reasonable (?)

[marco-vassena]

@AndreasLoowhttps://github.com/AndreasLoow @simonr89https://github.com/simonr89 I agree that one should commit to do more than 10 minutes. Splitting a session in, say, two presentations + time for discussion could be reasonable (?)

I think we could take this as a guideline, but I would not be too strict about it. Depending on the topic (open-ended vs basic) one could probably spend more time in one over the other.

Shall we get in touch with Thierry for an estimate on the credits and comments about the course?

Marco

On 27 Feb 2017, at 17:28, Irene Lobo Valbuena notifications@github.com<mailto:notifications@github.com> wrote:

Excuse the lack of responses from my part. I was away and disconnected the whole of last week (the reason behind my lack of time for the slot this week).

@AndreasLoowhttps://github.com/AndreasLoow @simonr89https://github.com/simonr89 I agree that one should commit to do more than 10 minutes. Splitting a session in, say, two presentations + time for discussion could be reasonable (?)

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHubhttps://github.com/vlopezj/coq-course/issues/12#issuecomment-282771052, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AFN09oCt1OAXucO9ssqX7YOhxpCoulffks5rgvmrgaJpZM4L3LBI.

[AndreasLoow]

Shall we get in touch with Thierry for an estimate on the credits and comments about the course?

Is there much to comment on yet? Do we have a proper schedule yet? I think the people active in the course should pick a topic and add it -- and themselves -- to the schedule document. One does not have to pick a specific date, but picking a topic (or two, in the case of shorter presentations) would be very helpful I think; of course, one can change one's mind later, but this would give us some kind of overview of the things to be covered.

[AndreasLoow]

I just looked at the syllabus/plan, and as we have reached the (strong) normalization proof for simply typed lambda calculus in SF we are without a clear goal (again, :p, at least after potentially more ssreflect material). But there are a few interesting things going on in CPDT imho. Maybe one could have chap. 10 "Reasoning About Equality Proofs" and chap. 12 "Universes and Axioms" for one session? Heterogeneous equality (etc.) and type vs. prop vs. set still confuses me at least :). And, of course, the CPDT proof style is interesting to compare with the style from SF and what the ssreflect people are doing.

Note that this is a fairly uninformed suggestion, as I'm not sure how "jumpable" (in terms of dependencies) the chapters in CPDT are. But I think it should be doable. (One potential problem is that CPDT does not provide exercises as done in SF.)