David Baelde gave a talk at LF meeting today about focusing and least- and greatest-fixedpoint operators μ and ν. Neat stuff, but I can't get the hang of these awful spaghetti-pile classical focusing arguments. Frank came up with a beautiful constructive argument for the ccompleteness of focusing for ordinary intuitionistic logic that comes out to some 3rd-order (!) twelf code. Independently and just afterwards I found something very similar which is only 2nd-order but has the slight disadvantage that it calls out to cut. In hindsight this is to be expected, since Frank's proof "bakes in" the cut in the same way as some intrinsic twelf presentations of callcc.