Lambda the Ultimate

Hi,

I have a question: what're the benefits of investigating type theories when designing new programming construct/model/paradigm? I read through some of the recent interesting papers posts on LtU. Always, the authors dedicate a section to formalize their new programming constructs under various lambda calculi. I'm asking this from the perspective that how does this help us in designing better programming languages? What kind of insights will such process of formalisation give us?

I'm genuinely interested in understanding this. I've been considering of doing a PhD in investigating better programming constructs. I can say I know untyped lambda calculus. Beyond that, I'm not particular strong in "deeper" type theories and other formal systems (e.g. denotational semantics). I'm wondering how a PhD thesis will stand up if it isn't strong in this aspect.

If I want to brush up my skills/knowledge in this area, I suppose the text "Types and Programming Languages"
by Benjamin C. Pierce will be my starting point? Any other suggestions?
--
John

Would a Alice-like language without value cells but with monadic state have any advantages over Haskell?

It seems that Alice's combination of strict, lazy, and lenient evaluation, coupled with transparent futures would make it more powerful than plain Haskell.

Thanks.

Analyzing the Environment Structure of Higher-Order Languages using Frame Strings, Matthew Might and Olin Shivers. 2007.

Reasoning about program behaviour in programming languages based on the lambda-calculus requires reasoning in a unified way about control, data and environment structure. Previous analysis work has done an inadequate job on the environment component of this task. We develop a new analytic framework, Delta-CFA, which is based on a new abstraction: frame strings, an enriched variant of procedure strings that can be used to model both control flow and environment allocation. This abstraction enables new environment-sensitive analyses and transformations that have not been previously attainable. We state the critical theorems needed to establish correctness of the entire technology suite, with their proofs.

Even if you're not interested in flow analysis of functional languages, the preface to this paper is very enjoyable reading. (If you are interested in flow analysis, the whole thing is enjoyable reading. I want a couple of weeks to go through this paper in detail.)