Random half-thought: I wonder if something like argument maps would be a less intimidating notation for defining programming language semantics than natural deduction: en.wikipedia.org/wiki/Argument_
Conversation
I'm imagining that you would define a series of 'nodes' for your argument map. With terminal nodes for your axioms. These would be your inference rules. The inputs and outputs of your nodes would follow the syntax of your language. You'd then wire them together to form proofs.
3
Isn't this proof nets (more or less)?
1
Could be! 🧐
1
Replying to
When you and Girard are on the same page it is usually a good sign (when it comes to logic anyway) :)
1
Yeah, not surprised at all that it’s not new. Just wondering if I could define a language spec using them. Kinda like railroad diagrams!