Stream: Coq users

Topic: learning Coq


view this post on Zulip Robert Watson (Nov 08 2022 at 23:13):

Hello all, I've got up to the chapter called Simple Imperative Programming in Pierce's Logical Foundations (self study). This chapter introduces tacticals and deals with some larger problems. I am suddenly finding it much harder than all the other previous parts of the book and previous exercises. I don't want to start skipping over bits. Any advice as to how to get through this barrier?

view this post on Zulip Karl Palmskog (Nov 09 2022 at 07:14):

not sure there is a general method, but it might be helpful to look at similar educational material: https://github.com/coq-community/awesome-coq#books (other course material just below in that link)

view this post on Zulip Pierre Courtieu (Nov 09 2022 at 15:19):

The imperative language semantics is indeed a "big" example in logical foundation. You might skip it for a while but it is the main subject of the next book (software foundation). So if you intend to continue the book series you will need to dive into it anyways.

You may just need to read a few other introductory material on this subject to keep going. Nothing really hard is at stake here, really. Just understanding that describing the meaning of a program is not really different than describing the meaning of a formula.

There are plenty of sources. The first 20 pages of this came up first in the web.


Last updated: Jan 28 2023 at 08:02 UTC