Workshop on LEAN oriented towards CSLib Contribution

Stream: CSLib

[Sati]

Hello, all. I am from IIT Gandhinagar. We're interested in hosting a workshop on LEAN4 specifically oriented towards using and contributing to CSLib. The motivation for this is that (as far as I know) a lot of the current material on LEAN is either on the functional programming aspects within LEAN itself, oriented towards primarily mathematicians, or related to PL Theory specifically.

I don't think the 3 goals stated in CSLib are captured by these appropriately, and it would be nice to work on something that does. This would require some careful thought about structure and pacing (For example, one could consider a tutorial on Aeneas in the workshop with respect to goal 3).

I would appreciate comments and critiques on this idea. Invitations to help are welcome too! Thanks a lot!

(PS: I'm expecting that the audience will be students from both the undergraduate and postgraduate levels.)

[Shreyas Srinivas]

I think it’s a bit too early to host a workshop since we are still working on foundational aspects of CSLib and a lot of it is still in flux. A workshop makes more sense when we are all largely committed to basic definitions to some extent and we are asking contributors to contribute things like specific algorithms or theorems.

[Shreyas Srinivas]

But that’s just my opinion

[Fabrizio Montesi]

Sati said:

Hello, all. I am from IIT Gandhinagar. We're interested in hosting a workshop on LEAN4 specifically oriented towards using and contributing to CSLib. The motivation for this is that (as far as I know) a lot of the current material on LEAN is either on the functional programming aspects within LEAN itself, oriented towards primarily mathematicians, or related to PL Theory specifically.

I don't think the 3 goals stated in CSLib are captured by these appropriately, and it would be nice to work on something that does. This would require some careful thought about structure and pacing (For example, one could consider a tutorial on Aeneas in the workshop with respect to goal 3).

I would appreciate comments and critiques on this idea. Invitations to help are welcome too! Thanks a lot!

(PS: I'm expecting that the audience will be students from both the undergraduate and postgraduate levels.)

To understand how we could support you, do you have any thoughts about what the course could cover about our current codebase?

[Sorrachai Yingchareonthawornchai]

There is some attempt to create Lean material towards proving the analysis of algorithms. You can check from here.

[Eric Wieser]

Are there plans to update that repo to use the TimeM defined in CSLib?

[Sati]

Fabrizio Montesi said:

Sati said:

Hello, all. I am from IIT Gandhinagar. We're interested in hosting a workshop on LEAN4 specifically oriented towards using and contributing to CSLib. The motivation for this is that (as far as I know) a lot of the current material on LEAN is either on the functional programming aspects within LEAN itself, oriented towards primarily mathematicians, or related to PL Theory specifically.

I don't think the 3 goals stated in CSLib are captured by these appropriately, and it would be nice to work on something that does. This would require some careful thought about structure and pacing (For example, one could consider a tutorial on Aeneas in the workshop with respect to goal 3).

I would appreciate comments and critiques on this idea. Invitations to help are welcome too! Thanks a lot!

(PS: I'm expecting that the audience will be students from both the undergraduate and postgraduate levels.)

To understand how we could support you, do you have any thoughts about what the course could cover about our current codebase?

Looking at the current codebase I think the most accessible and easy to approach things would be the TimeM monad and the Deterministic Automata (and possibly the Lambda Calculus).

There is also the Boole Sandbox branch, I think it'd be of great value to use it to talk about program verification. But I'm not sure if it'd be advisable to cover it if the syntax and semantics are still experimental.

[Sati]

Sorrachai Yingchareonthawornchai said:

There is some attempt to create Lean material towards proving the analysis of algorithms. You can check from here.

This is useful. Thanks!

[Clark Barrett]

For Boole, we are working hard to get a set of simple examples working with our infrastructure. Depending on the timing of your course, we may be far enough along for people to try it out and play with it.

[Sati]

Well we're looking to conduct only a small workshop by the end of March, hopefully

[Sati]

It'd be a part of the activities of the club, so it serves both as an introduction to LEAN and theorem proving for computer science undergraduate students, and an invitation to do more in depth work. So it may be fine to talk about experimental stuff just so people who've never seen anything like this before get an idea of what it looks like, if that makes sense.

[Clark Barrett]

If you want to try some experimental stuff, you can try out some of the Boole examples in the Boole-sandbox branch. You can start here: https://github.com/leanprover/cslib/blob/Boole-sandbox/Cslib/Languages/Boole/README.md. Feel free to reach out if you have problems getting things set up.

[GasStationManager]

You might also be interested to check out my collection of algorithms at https://github.com/GasStationManager/ArtificialAlgorithms/
The goal of the repo is more AI focused, but i imagine might also be useful to students..