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?