3 ms·
One of the most amazing things about linear logic is that "classical" linear logic has a direct constructive reading. This has some interesting applications in
by fmap 8y ago
One of the most amazing things about linear logic is that "classical" linear logic has a direct constructive reading.
This has some interesting applications in constructive mathematics (https://arxiv.org/abs/1805.07518 https://arxiv.org/abs/1805.07518) and programming (http://homepages.inf.ed.ac.uk/wadler/papers/multiparty/multiparty.pdf http://homepages.inf.ed.ac.uk/wadler/papers/multiparty/multi...).
- carterschonwald 8y agoThe Shulman paper was the first instance I’ve seen of someone properly using Par in their logical modelling I’ve been slowly working on some applied linear logic stuff for my day job the past two years. I definitely think a lot of work has missed out on what happens if you have both implication and par native to your system. You get a really nice kernel for a concurrent functional programming language. With nice resource safety.
- fmap 8y agoI couldn't agree more, classical linear logic leads to surprisingly concise definitions. Your day job sounds fascinating, would you mind expanding on it a bit?