Would it be helpful to suggest topics in Github or here?

Stream: CSLib

[Jason Carr]

I'm in PLT, and there's a few gaps I didn't see represented much, particularly in the space of compilers and modern semantics.

• System Fω; termination of F, Fω, which then requires logical relations
• Operational semantics: sequential CESK machine (very hard to define generically), ANF or CPS-style functional language parametrized over primitive ops would work.
  • Probably want to compile this to Boole as well
  • Or give Boole semantics into CESK; although Iris uses effectively a parallel "CS" machine
• Abstract interpretation notions for any transition system + soundness
• parametrized AAM for the CESK machine

I guess the main thing is representation of essential compilers and program analysis constructions, whereas Boole is focused on verification, and focused on imperative languages.
Imperative languages themselves usually eliminate things like local refs into join points, although SSA is more common for imperative compilers (but it's harder to scope check than ANF/CPS

Also noting that the plan for Boole overlaps partially but maybe synergizes with Iris which is being copied over to Lean (it is mostly language-agnostic fortunately)

[Shreyas Srinivas]

Logical relations would be cool to have in CSLib. But they are also horrendous to formalise. I still have occasional nightmares from my semantics course. If you pull that off that would be brilliant. I understand @Chris Henson already has some working code on System F

[Chris Henson]

To answer the question in the title, discussion here is probably easiest.

Logical relations can be tricky, but I personally don't think they are too onerous to formalize in these relatively simple type systems and they are more than welcome in CSLib.

Specifically we have System F with subtyping and a couple of other extensions, done with locally nameless binding. I mentioned in another thread that Fω and its termination would be a welcome addition. Maybe it would be easiest to work with locally nameless for the time being and follow what's already been done, but we can coordinate if you're really wanting to do something like well scoped indices. (The context here is I'm working on something like Autosubst for Lean).

I am not involved with Boole, but the other areas like CESK machines seem straightforwardly welcome in CSLib. I don't think anyone else has me mentioned working on this, so I'd say go for it if you are interested! You can always open a draft PR for early feedback. For completely new modules, it's always a bit of a balancing act between keeping it reasonably small and proving something slightly nontrivial to sanity check the definitions.

[Fabrizio Montesi]

Agreed. Only one additional note: please try to keep each discussion as small as reasonably possible, since some of the topics you mention can be separated.
We care about design so if you're in doubt about anything or would just like to spar, you're more than welcome to open a topic here.