Status report

Stream: concrete semantics

[Simon Hudon]

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

[Simon Hudon]

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

[Jasmin Blanchette]

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":

https://github.com/blanchette/logical_verification_2019

And our still rapidly evolving lecture notes at

https://github.com/blanchette/logical_verification_2019/blob/master/logical_verification_in_lean.pdf

[Simon Hudon]

Thanks!