4 ms·
Lean 4 uses FBIP, but it looks like this paper is about something called FIP, which is related but about guaranteeing there are no allocations or deallocations.
by kmill 3y ago
Lean 4 uses FBIP, but it looks like this paper is about something called FIP, which is related but about guaranteeing there are no allocations or deallocations. FBIP as I understand it is more about being able write functional code in a natural away while avoiding allocations or deallocations.
(I agree about Lean 4 as becoming a great general purpose language though!)
- francasso 3y agoI'm sure the details are different, but the general idea, to me, seems the same as the one descibed by Leo and Sebastian in https://arxiv.org/abs/1908.05647 https://arxiv.org/abs/1908.05647. Both Koka and Lean 4 use reference counting to know if it's safe to reuse a structure. This paper (Daan is a collegue of Leo at MS Research) gives a different formalization and proofs. The file is still named "fbip.pdf" though :)