Ideas on integrating dependent types w/ low level programs?

Stream: Real-time Systems

[Jason Qin]

Looking for some ideas on using enhanced types with something like lean to model desirable properties relevant in lower level programming and embedded programming. Things like thread and memory safety a la rust but with perhaps a more comprehensive or modifiable design. Maybe encoding safe references as types. Or functions that take in a heap allocator that ensures all allocated memory is deallocated at some point. Threads with an ID attached to them and that no memory can be read and written by two different threads simultaneously.

[Shreyas Srinivas]

Are cache coherence protocols your cup of tea? Since you say "like Lean", there's the following : http://adam.chlipala.net/papers/HemiolaCAV22/

[Karl Palmskog]

FCSL has done low-level concurrency in Coq for some time: https://software.imdea.org/fcsl/