Lambda the Ultimate

While not strictly related to programming languages, some people might be interested in Computability Logic, which purports to generalize classical, linear and intuitionistic logics in a unified formal theory of computability. Brief overview:

Computation and computational problems in Computability Logic are understood in their most general, interactive sense, and are precisely seen as games played by a machine (computer, agent, robot) against its environment (user, nature, or the devil himself). Computability of such problems means existence of a machine that always wins the game. Logical operators stand for operations on computational problems, and validity of a logical formula means being a scheme of "always computable" problems. [...] The classical concept of truth is nothing but a special case of computability -- computability restricted to problems of zero interactivity degree.

Looks like an interesting approach, and intuitively appealing, at least to me. Here's a link to the first paper Introduction to computability logic, by Giorgi Japaridze:

This work is an attempt to lay foundations for a theory of interactive computation and bring logic and theory of computing closer together. It semantically introduces a logic of computability and sets a program for studying various aspects of that logic. The intuitive notion of (interactive) computational problems is formalized as a certain new, procedural-rule-free sort of games (called static games) between the machine and the environment, and computability is understood as existence of an interactive Turing machine that wins the game against any possible environment. The formalism used as a specification language for computational problems, called the universal language, is a non-disjoint union of the formalisms of classical, intuitionistic and linear logics, with logical operators interpreted as certain, — most basic and natural, — operations on problems. Validity of a formula is understood as being “always computable”, and the set of all valid formulas is called the universal logic. The name “universal” is related to the potential of this logic to integrate, on the basis of one semantics, classical, intuitionistic and linear logics, with their seemingly unrelated or even antagonistic philosophies. In particular, the classical notion of truth turns out to be nothing but computability restricted to the formulas of the classical fragment of the universal language, which makes classical logic a natural syntactic fragment of the universal logic. The same appears to be the case for intuitionistic and linear logics (understood in a broad sense and not necessarily identified with the particular known axiomatic systems). Unlike classical logic, these two do not have a good concept of truth, and the notion of computability restricted to the corresponding two fragments of the universal language, based on the intuitions that it formalizes, can well qualify as “intuitionistic truth” and “linear-logic truth”. The paper also provides illustrations of potential applications of the universal logic in knowledgebase, resourcebase and planning systems, as well as constructive applied theories. The author has tried to make this article easy to read. It is fully self-contained and can be understood without any specialized knowledge of any particular subfield of logic or computer science.

Edit: I just realized there was an LtU post on this in the past (and another one), but if you haven't seen it already, it's worth a look!