Is there formalization of data structures and algorithms?

Stream: lean4

[Guchan Li]

Hello! Since Lean 4 can describe almost all mathematical structures, I am wondering is there existing works that formalizes data structures and algorithms in computer science? I see there are lists and binary trees, but are there more rigorous ones? For example, is it possible to describe Dijkstra's shortest path algorithm, and argue about its computational complexity? I would be excited to discuss these with you! :smile:

[Chris Henson]

The #CSLib library is still setting up foundations for this sort of work, with two different approaches: a deep embedding of an imperative language and a monadic representation.

[Guchan Li]

Cool! I'll switch to that channel.