Lambda the Ultimate

Define dead-end theorems to be theorems that are not used to prove other results. What percentage of proofs in PLT papers are of dead-end theorems?

For example, a type soundness result is not often used to prove more fundamental results. It is just a "house keeping" theorem.

Does this percentage tell us anything important?

I'm most familiar with the Common Lisp style implementation of the multiple-value-return feature.

But I notice that several other languages, including Python, use tuple return values and do destructuring on these tuples.

What are the advantages/disadvantages to each? Semantically? Implementation and performance?

Are there other (better) models of multiple-value-return that I should study?

Thanks much!

Scott
- No, I'm not a student :-)