New answers tagged pl.programming-languages
1
You may be interested in the Kappa calculus which has no higher order maps and broadly corresponds to Cartesian categories. You might also want to look into co-intuitionistic logic which has "coexponentials." Unfortunately you can't combine "coimplication" and "implication" constructively. You need to weaken something somewhere ...
3
Such a logic of continuations (or a syntax of continuation that arose from logical considerations) would be Laurent's “polarised linear logic” (LLP): Olivier Laurent, Étude de la polarisation en logique (2002). A good explanation of what is going on from a categorical perspective is given in Melliès and Tabareau, Resource modalities in tensor logic (2010). A ...
3
For me, what is going on is reasonably standard:
You have $c$ with free variables $(x_i : \tau_i)_i$, and you replace it with $c[t_i/x_i]$ with the $(t_i)_i$ at types $(\tau_i)_i$; this is a standard cut/substitution.
The replacement is done along a variable $k$ that is defined somewhere and used elsewhere; this sort of "action at a distance" is ...
Top 50 recent answers are included