One elegant definition of the nonnegative integers standardly ordered is as the initial algebra of the functor 1;X, ordinal sum (concatenation) with the singleton. We give a construction dual to this for the nonnegative reals standardly ordered, namely as the final coalgebra of the functor X.w, ordinal (lexicographic) product with the natural numbers. This gives a sense in which analysis is dual to enumeration. Baire space and Cantor space are similarly obtained as final coalgebras of elaborations of this functor, respectively X'.w (order dual) and 1;(X.w), sitting on either side of the continuum. When combined as 1;(X'.w) the two elaborations cancel to restore the continuum.
Linear logic was introduced by Girard in 1987 as a resource-sensitive "logic behind logic". Chu spaces are a common generalization of topological spaces/finite dimensional vector spaces/abelian groups, etc. represented in terms of the relationship between their points and open sets/functionals/group characters, etc.
We put the syntactic proofs of the theorems of multiplicative linear logic in one-one correspondence with their semantic proofs defined as logical transformations between operations on Chu spaces. One can view a result of this nature as a refinement of ordinary completeness to a characterization of proofs rather than of mere provability.
Joint work with Harish Devarajan, Gordon Plotkin, and Vaughan Pratt.
Second half of talk on Chu spaces (see previous abstract).