cslib

Stream: general

[Notification Bot]

This topic was moved to #computer science > cslib by Bryan Gin-ge Chen.

[Yaël Dillies]

Congratulations, @Fabrizio Montesi!

[Yaël Dillies]

It looks like https://github.com/leanprover/cslib still points to cs-lean.github.io rather than leanprover.github.io/cslib

[Yaël Dillies]

Oh, is this expected?

[Fabrizio Montesi]

Yes, but it's a temporary solution.

[Fabrizio Montesi]

Yaël Dillies said:

Congratulations, Fabrizio Montesi!

Thanks! Extending to @Clark Barrett, @Swarat Chaudhuri, @Leonardo de Moura.

[Chris Henson]

Yes, thank you all for the idea to merge! I am very glad for my lambda calculi formalizations to be welcomed in the scope of this project. I will soon PR a locally nameless formalization of System F with subtyping (making good use of grind!) and have plans for CoC and other representations/systems.

[Eric Wieser]

For anyone else confused by Yael congratulating the thread being moved, there is an announce thread

[Ching-Tsun Chou]

Sorry, I'm a bit confused. As of now, is there any repo corresponding to the CSLib announcement (#CSLib > Announcing CSLib )?

[Chris Henson]

Ching-Tsun Chou said:

Sorry, I'm a bit confused. As of now, is there any repo corresponding to the CSLib announcement (#CSLib > Announcing CSLib )?

https://github.com/leanprover/cslib contains the work that @Fabrizio Montesi announced as being merged into the project, but no, the portion originally discussed in that channel has not yet been made public.

[Shreyas Srinivas]

does this mean we can start contributing to CSlib?

[Ching-Tsun Chou]

It may be a good idea to wait for Amazon to release their code.

[Chris Henson]

Shreyas Srinivas said:

does this mean we can start contributing to CSlib?

I'll defer to the project owners, but while aspects like the Boole DSL are not yet public, I think other PRs not dependent on this are welcome? For instance @Thomas Waring and @Matt Diamond have been working on different variations of Rice-Shapiro, myself on lambda calculi, etc.

[Fabrizio Montesi]

As Chris said, the codebase starts from what we had in cs-lean/cslib. We'll integrate Boole as soon as it's ready to be published.

Re contributions: We're open for contributions! There are so many things to cover and so many improvements that we could use for what is already in the codebase. Please feel free to open topics to discuss ideas.
If you wanna formalise the correctness of an imperative sequential algorithm/data structure, it's worth waiting a bit for Boole.

[Swarat Chaudhuri]

As it happens, Amazon has already released the Strata platform (which we referred to by a different name during the community calls): https://github.com/strata-org/Strata/tree/main. Boole will be a "dialect" of Strata and we are actively discussing what it will exactly look like. As @Fabrizio Montesi said, please start contributing foundational CS-relevant formalizations, but if you want to formalize properties of code (including algorithms + data structures), it would be useful to wait.

[Shreyas Srinivas]

I was wondering if it would make sense for me to merge our algebraic complexity repository into this.

[Shreyas Srinivas]

It’s an area of complexity theory that deals with the size and depth of arithmetic circuits computing a given polynomial. I still need to check with my collaborators before committing to it, but I can see some benefits.

[Shreyas Srinivas]

Whether this qualifies as “undergrad CS” is up for debate.

[Fabrizio Montesi]

It doesn't need to be about undergrad CS anymore, after the merge. We already have things that go beyond it anyway.

Please feel free to open a topic in the computer science or cslib channels to discuss this. Do you have a pen-and-paper reference and code we can look at?

[Shreyas Srinivas]

A part of the code is already online. I can upload some more of mine later this weekend

[Shreyas Srinivas]

But I will first discuss this with my collaborators

[Shreyas Srinivas]

I just need to know if it even makes sense to raise the topic with them

[Swarat Chaudhuri]

Yeah, even before the merge, "undergrad CS" was meant to be a milestone rather than an endpoint. We are free to overshoot that goal. :slight_smile:

[Kevin Buzzard]

"undergrad math" was a milestone for mathlib at the beginning (and the milestone is still not complete!), but now we have a huge amount of non-undergrad math.

[Shreyas Srinivas]

I have obtained permission to merge pieces of algebraic-complexity as we make progress. But we would like to fix some proofs, reach some goals, and publish them before merging it all.

[Jafar Tanoukhi]

Hi, I’m interested in the cslib project. Is it currently open for contributions? I noticed there are only two issues listed, so I wasn’t sure if it's accepting contributions or not mature enough for that yet?

[Clark Barrett]

We are laying some groundwork and expect to issue a call for contributions soon. Stay tuned!

[Jafar Tanoukhi]

Clark Barrett said:

Stay tuned!

Oh, alright. Any suggestions on what could be done in the meantime? I am still quite a beginner in lean (finished NNG and made my first mathlib PR with a coauthor), but very interested in getting into more theoretical parts of CS (I am a graduate; starting my masters soon at one point, but currently work as a developer).

[Clark Barrett]

You can already start looking at the github repo: leanprover/cslib

[Fabrizio Montesi]

Some pointers:
I've left some proof_wanted in CCS, if you wanna have a look. We also still miss a proof of cut elimination for linear logic, but that's hard if you're not an expert in it.