Hacker News Reader

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) and programming (http://homepages.inf.ed.ac.uk/wadler/papers/multiparty/multi...).

View on HN

The 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.

I 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?

Reply on news.ycombinator.com