addressalign-toparrow-leftarrow-rightbackbellblockcalendarcameraccwcheckchevron-downchevron-leftchevron-rightchevron-small-downchevron-small-leftchevron-small-rightchevron-small-upchevron-upcircle-with-checkcircle-with-crosscircle-with-pluscontroller-playcrossdots-three-verticaleditemptyheartexporteye-with-lineeyefacebookfolderfullheartglobegmailgooglegroupshelp-with-circleimageimagesinstagramFill 1light-bulblinklocation-pinm-swarmSearchmailmessagesminusmoremuplabelShape 3 + Rectangle 1ShapeoutlookpersonJoin Group on CardStartprice-ribbonprintShapeShapeShapeShapeImported LayersImported LayersImported Layersshieldstartickettrashtriangle-downtriangle-uptwitteruserwarningyahoo

Do chapters 6 and 8 (Logic and Prop) of Software Foundations

  • Aug 25, 2014 · 7:00 PM
  • Mixrank

The Logic and Prop chapters of Software Foundations clarify some of the Coq basics we've been skirting around till now. I don't claim that using Coq won't feel like playing Adventure after we've done these chapters, but we might at least feel like more experienced players.

Note that I'm basing the chapter numbers on the July 2014 issue of Software Foundations, which inserts another chapter (Rel, on properties of relations) in between Logic and Prop. Having skimmed all three chapters, though, I think it makes more sense to postpone Rel.

And don't forget that gate code! *1111 will get you into Mixrank.

Join or login to comment.

  • Christopher B.

    With regret, I won't make it tonight. Was already feeling insufficiently prepared, then discovered there is a Giants game tonight that will again push up parking meter rates to $7 an hour.

    August 25, 2014

    • Ian Z.

      Probably the level of negation :)

      August 25, 2014

    • Adrian K.

      Negation is my weakness too. I just have to keep repeating: ex falso quodlibet. Ex falso quodlibet...

      August 25, 2014

  • Adrian K.

    I'm having some trouble with negation (perhaps because I always try to keep an upbeat, constructive attitude) -- anyone have any clue how to get started on excluded_middle_irrefutable in the Logic chapter? The obvious opening "intros. unfold not. intros. apply H." just leads you to the law of excluded middle, which you can't prove.

    August 24, 2014

    • A former member
      A former member

      Are the sessions recorded?

      August 25, 2014

    • Adrian K.

      Alas, the sessions are not recorded. It would be a little difficult to make a coherent recording with the Coq track anyway; there's no single lecturer, just people talking about the homework.

      August 25, 2014

  • Mark W.

    This meetup sounds awesome, but I'm a little worried about being behind. Is it necessary to be immediately caught up in the textbook?

    August 19, 2014

    • Adrian K.

      If we do want to start another section of the Coq track, this is our chance to have it some time other than Monday evening and/or someplace other than San Francisco.

      August 20, 2014

    • Adrian K.

      Mark, I think the main thing to remember when starting out with Coq is that many of the tactics do more than you might expect from their names, which makes their behavior a little mysterious. But if you keep trying different tactics, you can usually brute-force your way through a proof somehow.

      August 20, 2014

  • Sergei W.

    I miscalculated my travel schedule (I will be just arriving to SF at the meetup time). So I won't be able to make it this time, to my deep regret.

    August 16, 2014

3 went

People in this
Meetup are also in:

Sign up

Meetup members, Log in

By clicking "Sign up" or "Sign up using Facebook", you confirm that you accept our Terms of Service & Privacy Policy