Zulip Chat Archive

Stream: concrete semantics

Topic: hello

Welcome Bot (Feb 28 2019 at 17:27):

Welcome to #concrete semantics.

Simon Hudon (Feb 28 2019 at 17:29):

I'd like a group reading of "Concrete Semantics" and do the exercises at a rhythm of ~one chapter a week

Kevin Buzzard (Feb 28 2019 at 17:35):

Is that this http://concrete-semantics.org/ concrete semantics or another one?

Mario Carneiro (Feb 28 2019 at 18:56):

are the exercises in isabelle?

Jeremy Avigad (Feb 28 2019 at 20:33):

It would be great to have versions of the examples and exercises in Lean.
BTW, does anyone recognize the tenement building on the cover? Hint: Tobias and I share a deep appreciation of Led Zeppelin.

Simon Hudon (Feb 28 2019 at 20:33):

The exercises are in Isabelle but I plan to do them in Lean

Simon Hudon (Feb 28 2019 at 20:34):

@Kevin Buzzard that's the one

Simon Hudon (Feb 28 2019 at 20:35):

@Jeremy Avigad It looks sort of familiar but I can't put my finger on what album it reminds me of

Jeremy Avigad (Feb 28 2019 at 20:35):

https://en.wikipedia.org/wiki/Physical_Graffiti

Jeremy Avigad (Feb 28 2019 at 20:36):

A student of Tobias' actually went to NY and took a picture of the same building.

Simon Hudon (Feb 28 2019 at 20:36):

Ah! :D We should put it on in your office next time we jam on the board :D

Simon Hudon (Feb 28 2019 at 20:40):

If there is enough interest at CMU / Pitt, I'd do a weekly meeting to see what people have a hard time with

Kevin Buzzard (Feb 28 2019 at 20:51):

Physical Graffiti :-) My favourite Zep album!

Kevin Buzzard (Feb 28 2019 at 20:51):

Oh, I just noticed you posted the answer :P I got it independently, I swear!

Joe Kiniry (Apr 30 2021 at 21:54):

I'm afraid that http://concrete-semantics.org/ is done these days. Perhaps someone should nudge Tobias or Gerwin.

Mario Carneiro (Apr 30 2021 at 22:44):

what do you mean by "done"?

Joe Kiniry (Apr 30 2021 at 22:51):

s/done/down/

Last updated: Dec 20 2023 at 11:08 UTC