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 is held abstract, it works a lot like 'false' in that there is no introduction rule for it.

With respect to the paper you linked (I'm by no means an expert on it, and just skimmed it, really), I think it might help to study the reduction rules. It appears to me that the goal of the logic is to construct an expression $e : +\mathsf{int}$ and reduce that expression to a numeral $n$. This means that the continuation $\bullet : ¬int$ is not something that would be valid as a program in itself. Rather it is a clue that the abstract 'result type' is actually $\mathsf{int}$, because we are interested in using continuation-based computations that eventually result in integers. $\bullet$ is something that immediately completes the computation, hence the rules:

$$(begin)\ \ \ \ e : +int \leadsto \langle e | \bullet \rangle$$ $$(end)\ \ \ \ \langle n | \bullet \rangle \leadsto n$$

I don't know what happens if you have $\bullet$ involved in other situations, or if you can, but I might expect it to abort other continuations and end the computation. It seems more like it can only be the initial continuation based on the rules, though.

Now, one answer to your question is that this system is not even trying to reason about uninhabited types. It is using a correspondence between the logical rules and control flow, without the specific semantic meaning of negation. One thing you might want to check out is linear logic, because it actually has two sorts of 'false' or zero, one which is about control flow, and one which is about emptiness. The linearity is important for keeping them separate.

In that setting, $⊥$ is the 'false' that has to do with control flow, and it gets things like double negation elimination and excluded middle (with a corresponding 'or' that is more related to representing functions via continuations than it is disjoint union), while there is also $0$, which gets the principle of explosion (which is arguably the distinct part of the empty type). An interesting thing about this setting is that even though the logic seems classical, it is actually constructive because of the more restricted rules. Double negation by the 'control flow' bottom $⊥$ is just a different (possibly more convenient) way of structuring a program that computes the doubly-negated type (and 'excluded middle' is a decomposed identity function).

Fillinski's 'Linear Continuations' might be a good place to start reading, although there are probably other references as well.

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 is held abstract, it works a lot like 'false' in that there is no introduction rule for it.

With respect to the paper you linked (I'm by no means an expert on it, and just skimmed it, really), I think it might help to study the reduction rules. It appears to me that the goal of the logic is to construct an expression $e : +\mathsf{int}$ and reduce that expression to a numeral $n$. This means that the continuation $\bullet : ¬int$ is not something that would be valid as a program in itself. Rather it is a clue that the abstract 'result type' is actually $\mathsf{int}$, because we are interested in using continuation-based computations that eventually result in integers. $\bullet$ is something that immediately completes the computation, hence the rules:

$$(begin)\ \ \ \ e : +int \leadsto \langle e | \bullet \rangle$$ $$(end)\ \ \ \ \langle n | \bullet \rangle \leadsto n$$

I don't know what happens if you have $\bullet$ involved in other situations, or if you can, but I might expect it to abort other continuations and end the computation. It seems more like it can only be the initial continuation based on the rules, though.

Now, one answer to your question is that this system is not even trying to reason about uninhabited types. It is using a correspondence between the logical rules and control flow, without the specific semantic meaning of negation. One thing you might want to check out is linear logic, because it actually has two sorts of 'false' or zero, one which is about control flow, and one which is about emptiness. The linearity is important for keeping them separate.

In that setting, $⊥$ is the 'false' that has to do with control flow, and it gets things like double negation elimination and excluded middle (with a corresponding 'or' that is more related to representing functions via continuations than it is disjoint union), while there is also $0$, which gets the principle of explosion (which is arguably the distinct part of the empty type¹). An interesting thing about this setting is that even though the logic seems classical, it is actually constructive because of the more restricted rules. Double negation by the 'control flow' bottom $⊥$ is just a different (possibly more convenient) way of structuring a program that computes the doubly-negated type (and 'excluded middle' is a decomposed identity function).

Fillinski's 'Linear Continuations' might be a good place to start reading, although there are probably other references as well.

1. In the continuation-with-abstract-result-type setting, you can also interpret explosion, but it has sort of a different meaning. Effectively such interpretations are always 'delimited' somewhere, even if it's only the end of your program. Explosion means that if you somehow get a value of the abstract result type, you can throw away your current continuation and jump to the delimiter. So it is an 'abort' operation. Linear logic doesn't allow this; all continuations must be used (and used exactly once), so explosion must be justified by involving an 'impossible' situation, like having a value of an empty type.

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 is held abstract, it works a lot like 'false' in that there is no introduction rule for it.

With respect to the paper you linked (I'm by no means an expert on it, and just skimmed it, really), I think it might help to study the reduction rules. It appears to me that the goal of the logic is to construct an expression $e : +\mathsf{int}$ and reduce that expression to a numeral $n$. This means that the continuation $\bullet : ¬int$ is not something that would be valid as a program in itself. Rather it is a clue that the abstract 'result type' is actually $\mathsf{int}$, because we are interested in using continuation-based computations that eventually result in integers. $\bullet$ is something that immediately completes the computation, hence the rules:

$$(begin)\ \ \ \ e : +int \leadsto \langle e | \bullet \rangle$$ $$(end)\ \ \ \ \langle n | \bullet \rangle \leadsto n$$

I don't know what happens if you have $\bullet$ involved in other situations, or if you can, but I might expect it to abort other continuations and end the computation. It seems more like it can only be the initial continuation based on the rules, though.

Now, one answer to your question is that this system is not even trying to reason about uninhabited types. It is using a correspondence between the logical rules and control flow, without the specific semantic meaning of negation. One thing you might want to check out is linear logic, because it actually has two sorts of 'false' or zero, one which is about control flow, and one which is about emptiness. The linearity is important for keeping them separate.

In that setting, $⊥$ is the 'false' that has to do with control flow, and it gets things like double negation elimination and excluded middle (with a corresponding 'or' that is more related to representing functions via continuations than it is disjoint union), while there is also $0$, which gets the principle of explosion (which is arguably the distinct part of 'negating' with the empty type). An interesting thing about this setting is that even though the logic seems classical, it is actually constructive because of the more restricted rules. Double negation by the 'control flow' bottom $⊥$ is just a different (possibly more convenient) way of structuring a program that computes the doubly-negated type (and 'excluded middle' is a decomposed identity function).

Fillinski's 'Linear Continuations' might be a good place to start reading, although there are probably other references as well.

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 is held abstract, it works a lot like 'false' in that there is no introduction rule for it.

With respect to the paper you linked (I'm by no means an expert on it, and just skimmed it, really), I think it might help to study the reduction rules. It appears to me that the goal of the logic is to construct an expression $e : +\mathsf{int}$ and reduce that expression to a numeral $n$. This means that the continuation $\bullet : ¬int$ is not something that would be valid as a program in itself. Rather it is a clue that the abstract 'result type' is actually $\mathsf{int}$, because we are interested in using continuation-based computations that eventually result in integers. $\bullet$ is something that immediately completes the computation, hence the rules:

$$(begin)\ \ \ \ e : +int \leadsto \langle e | \bullet \rangle$$ $$(end)\ \ \ \ \langle n | \bullet \rangle \leadsto n$$

I don't know what happens if you have $\bullet$ involved in other situations, or if you can, but I might expect it to abort other continuations and end the computation. It seems more like it can only be the initial continuation based on the rules, though.

Now, one answer to your question is that this system is not even trying to reason about uninhabited types. It is using a correspondence between the logical rules and control flow, without the specific semantic meaning of negation. One thing you might want to check out is linear logic, because it actually has two sorts of 'false' or zero, one which is about control flow, and one which is about emptiness. The linearity is important for keeping them separate.

In that setting, $⊥$ is the 'false' that has to do with control flow, and it gets things like double negation elimination and excluded middle (with a corresponding 'or' that is more related to representing functions via continuations than it is disjoint union), while there is also $0$, which gets the principle of explosion (which is arguably the distinct part of the empty type). An interesting thing about this setting is that even though the logic seems classical, it is actually constructive because of the more restricted rules. Double negation by the 'control flow' bottom $⊥$ is just a different (possibly more convenient) way of structuring a program that computes the doubly-negated type (and 'excluded middle' is a decomposed identity function).

Fillinski's 'Linear Continuations' might be a good place to start reading, although there are probably other references as well.