Migrated and expanded from a comment:
I think this must vary by subfield. Nearly all the Theory B stuff I'm familiar with (and especially Haskell, Agda, and sometimes Coq -related) includes published code, sometimes even as an appendix or better yet inlined within the paper. A fair number of papers from, e.g., ICFP are written as literate programs to begin with, and their source in its entirety is published by the authors. A fair amount of those in turn have resulted in extracted libraries for distribution.
Of the remaining papers, a fair amount never had code to begin with. Of those, there's probably two main reasons. First are the papers whose main content is proof trees, typing rules with associated soundness proofs and the like. Of those, advances in mechanized metatheory have encouraged at least some authors to provide code in their theorem prover of choice (see Weirich's slides on POPLmark: http://www.seas.upenn.edu/~sweirich/talks/cambridge-09.pdf). Second are those which are descended from the Bird-Merteens stuff (banannas & co.). These are generally translatable into a functional language without too much work. However, I suspect that there's both typically a loss of generality, and that dealng with concrete issues of syntax and typing needlessly complicates things and makes it harder to follow the equational reasoning.
I wanted to substantiate my observations a bit, so did a rough count of the first two days of ICFP 2010. Of standard papers (i.e. not experience reports or invited talks), 12 out of 21 provided code of some sort. Three provided Coq (a fourth claimed a partial proof but did not publish it). Three proided Haskell. Three provided Agda. One provided Scheme, one provided Caml, and one provided Twelf. (Note that some provided code for more than one proof assistant, or for both a formalization and an implementation). Of the remaining papers, a few did work at a high enough level of abstraction that implementing it in a proof assistant would be a new paper in itself, and a fair number more did work that I suspect could have been implemented in a proof assistant using standard techniques, but which certainly would have taken a fair amount of work to do so. A few further papers claimed implementations/releases as future work.