Zulip Chat Archive

Stream: concrete semantics

Topic: Status report

Simon Hudon (Mar 06 2019 at 22:03):

How far have people come? I'm done with chapter 3

Simon Hudon (Jan 11 2020 at 02:35):

@Harrison Grodin Hi! Here is the stream I was telling you about earlier

Jasmin Blanchette (Feb 07 2020 at 18:59):

BTW the parts on operational semantics, Hoare logic, and denotational semantics were the inspiration for the corresponding parts in our Lean course. The porting was done by Johannes Hölzl. You'll find our files here, in "lean/love{08,09,10}*.lean":


And our still rapidly evolving lecture notes at


Simon Hudon (Feb 07 2020 at 19:00):


Last updated: Dec 20 2023 at 11:08 UTC