Linear Logic
FinVect model
https://www.pls-lab.org/en/Vector_space_models_of_Linear_Logic https://www.seas.upenn.edu/~sweirich/types/archive/1992/msg00047.html
Cyclone Regions Tofte
Linear logic is resource sensitive. It is vaguely similar to
- Rust lifetimes
- Quantum information nad the no-cloning theorem
Can these be made precise?
It is realted to seperation logic in that both are substructural logics and in
It gives interesting insight into the proof search process of prolog and ilk.
Frank Pfenning had a funky example involving making change.
Chris Martens thesis Interactive worlds with linear logic strange loop talk ceptre Celf Ceptre stateful computation “frame property” all the stuff that strays the same purely functional - pass entire state datalog - database update celf - state update
Idris2 Linear haskell ATS Rust QTT - Quantitative type theory
Mercury has linear types of some kind
What if I modelled destructive rewrite rules in egglog as linear logical? Is a linear logic programmign langguae a good candidate for a prolog metainterpreter?