Denotational Semantics in Lean

Stream: CSLib

[Juanjo Madrigal]

Hi!

As a means to learn both Lean and Denotational Semantics, I've started to read the book "The Formal Semantics of Programming Languages" (Glynn Winskel, 1993) and translate all its concepts to Lean. It's on https://github.com/juanjomadrigal/denotational-lean ; I plan to upload some content every few days.

I have little experience with Lean so I'm sure it is terribly un-idiomatic and with lots of things to improve. Any feedback will be much appreciated :pray:

If after having much more content and after polishing etc. there is something that is useful as a formalized theory that can be contributed, that would be great.

Thank you!

[Shreyas Srinivas]

Mathlib has some elements of denotational semantics including Scott continuous functions and a lot of the lattice theory that goes into denotational semantics. You might want to explore what you could add to that

[Chris Henson]

Hi @Juanjo Madrigal! We definitely will have denotational semantics of various forms at some point. Winskel starts without binding, so this is probably a suitable place to start since you say you are new to both denotational semantics and Lean. Some of the semantics functions in chapter 5 may require a few tweaks to express them formally. One suggestion is to use one of the Mathlib developments on maps like docs#AList.

Regarding the direction Shreyas is indicating, I would point you towards these notes for later. I would like to have this in CSLib as well, but it is a bit more involved. I'd like to set up our well-scoped infrastructure before doing this.

[Juanjo Madrigal]

Great!! That's very interesting (and these notes look really nice). Thank you both for your comments :raised_hands:

@Shreyas Srinivas , you mean https://leanprover-community.github.io/con-nf/doc/Mathlib/Order/ScottContinuity.html , right?

Also, for improving my Lean code and receiving feedback, perhaps should I post it in general/new_members? Or do you recommend any other way?

[Chris Henson]

Yes, and there is docs#OmegaCompletePartialOrder. For various reasons, you might find it a bit difficult to work with if you're just learning Lean, but definitely something to look at.

If there is something CS-specific, maybe post in the computer science channel, otherwise new members is fine.

[Tanner Duve]

I would be happy to help in formalizing the notes you attached. I've studied a bit of domain theory. I'm unfamiliar with the "well scoped infrastructure", could you elaborate? @Chris Henson

[Chris Henson]

I mean well-scoped de Bruijn indices, where the type of terms is indexed by the number of free variables in scope. I'd like to have a PR this month giving an example for simple types so that further developments have a template to work from.

[Juanjo Madrigal]

The formalization of the book goes on well: first five chapters :partying_face: starting with Hoare rules

I'm not using the tools in Mathlib/Order; I'm essentially making everything I need to better grasp all the concepts. At the end I will adapt everything to Mathlib, and I hope I have then enough context in the subject to see whether there is something valuable to adapt for CSLib.

In the meanwhile, any advice to improvement is welcome :)

[Bas Spitters]

For Hoare logic you might want to look at std.do and loom.