Skip to main content
14 votes

Why is the Curry-Howard isomorphism?

I suspect someone is going to come along with a deep category-theoretic reason for the connection, but in the meantime, here is my insight. Both logic and programming with functions are built around ...
Joey Eremondi's user avatar
11 votes
Accepted

How do continuations represent negations (under the Curry–Howard correspondence)?

When one associates negation with continuations, it is probably not ideal to think of it in terms of an 'empty' type. Continuation passing can be done with respect to any result type, and if that type ...
Dan Doel's user avatar
  • 1,021
10 votes

Type-theoretic interpretation of Skolemization

Skolemization corresponds to the so-called type theoretic axiom of choice, which is briefly discussed in section 1.6 of the HoTT book. This provides an equivalence along which we can swap $\Sigma$ ...
András Kovács's user avatar
9 votes
Accepted

Motivation for Dependent Type

Actually, the motivation for introducing dependent types goes in the opposite direction! Curry had noticed that there was a direct correspondence between typed terms in the $SK$ calculus and proofs in ...
cody's user avatar
  • 13.9k
7 votes

Why is the Curry-Howard isomorphism?

Someone wanted a deep category-theoretic insight? A Heyting algebra is a cartesian-closed category.
Andrej Bauer's user avatar
  • 28.9k
5 votes
Accepted

What's the logical counterpart to jumps with arguments on CPS terms?

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 ...
gadmm's user avatar
  • 307
4 votes
Accepted

Languages that lack contraction, weakening or exchange

As other commenters have mentioned what you are actually asking for is a language for planar string diagrams, aka monoidal categories. But let me address your question purely from the point of view ...
Ross Duncan's user avatar
3 votes

What's the logical counterpart to jumps with arguments on CPS terms?

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 ...
gasche's user avatar
  • 2,040
3 votes

Languages that lack contraction, weakening or exchange

If you remove all those rules and add something like If $A \vdash B$ and $A' \vdash B'$ then $A, A' \vdash B, B'$ you get a logic essentially for monoidal categories (it's basically string diagrams ...
Izaak Meckler's user avatar
2 votes

Connection between strong normalization of the simply typed λ-calculus, and cut elimination for propositional logic

How “standard” is it? A post by Anupam Das on the proof theory blog attacks the folklore by comparing the following two results: Proposition 1 (Folklore). For any theorem A of IPL, we can compute a ...
gadmm's user avatar
  • 307
1 vote

What's the logical counterpart to jumps with arguments on CPS terms?

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 "...
Molly Stewart-Gallus's user avatar
1 vote

How do continuations represent negations (under the Curry–Howard correspondence)?

Actually, your question is too narrowly-focused. For intuitionist logic, and its underlying Heyting lattice, for any formula $X$, the subset of formulae $\overline{A} = A → X$ is a reverse-mapping of ...
NinjaDarth's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible