User loginNavigation 
The stack calculus : a fundamental (and simple !) calculus for Classical LogicAround April 1 (but doesn't seem like a joke) 2013, on arxiv: We introduce a functional calculus with simple syntax and operational semantics in which the calculi introduced so far in the Curryâ€“Howard correspondence for Classical Logic can be faithfully encoded. Our calculus enjoys confluence without any restriction. Its type system enforces strong normalization of expressions and it is a sound and complete system for full implicational Classical Logic. We give a very simple denotational semantics which allows easy calculations of the interpretation of expressions. I haven't looked at the details yet, but the result are surprisingly simple and look deeply interesting  if you're into that sort of thing. I was always a bit rebuted the relatively large size of classical calculi, with lots of rules on top of the lambdacalculus. This one doesn't have a lambda primitive (a bit like System L in this respect) and is surprisingly concise.
(Fun fact: intuitionistic calculi are structured by the fact that there is only one hypothesis on the right of the turnstile. They have at most one hypothesis on the left of the turnstile.)
By gasche at 20130402 15:20  LtU Forum  previous forum topic  next forum topic  other blogs  4439 reads

Browse archivesActive forum topics
New forum topics

Recent comments
8 hours 37 min ago
8 hours 48 min ago
1 day 14 hours ago
6 days 21 hours ago
1 week 1 day ago
2 weeks 5 days ago
3 weeks 4 days ago
4 weeks 4 days ago
6 weeks 2 days ago
6 weeks 5 days ago