This thesis establishes formal equational properties of multi-stage calculi and related proof techniques that support analyses of staged programs. A key promise of staging is to make programs efficient without destroying clarity, thereby reducing the likelihood of bugs. However, few publications rigorously verify that their staged programs indeed behave as intended. In fact, little is known about how staged programs can be verified, or what correctness issues staging introduces. To solve this problem, I show a reduction of the correctness of a staged program to that of an unstaged program. This reduction not only clarifies the effects of staging on program behavior but also eases verification, as unstaged programs are more susceptible to existing reasoning techniques. I also demonstrate that important single-stage reasoning techniques apply to staged programs. These techniques are useful for establishing side conditions for the reduction and for discovering or validating further reasoning principles. / NSF grant CCF-0747431

Multi-stage programming is a valuable technique for improving the performance of computer programs through run-time optimization. Current implementations of multi-stage programming do not support run-time type introspection, which is a significant feature of modern object-oriented platforms such as Java and C#. This is unfortunate because many programs that use type introspection in these languages could be improved with multi-staging programming. The aim of this research is to investigate the interaction between multi-stage programming and object-oriented type introspection. This is done by the invention of a new programming language that is a multi-stage extension to C#. The language is capable of expressing traditional multi-stage programs as well as a new style of multi-stage programs that incorporate type introspection, most notably polytypic algorithms such as object serialization. A compiler for the language is implemented and freely available. The language is significant because it is the first object-oriented, multi-stage language; the first attempt to combine type introspection with multi-stage programming; and the first exploration of polytypic programming in a multi-stage context.

Une approche classique pour traiter les problèmes d’optimisation avec incertitude à deux- et multi-étapes est d’utiliser l’analyse par scénario. Pour ce faire, l’incertitude de certaines données du problème est modélisée par vecteurs aléatoires avec des supports finis spécifiques aux étapes. Chacune de ces réalisations représente un scénario. En utilisant des scénarios, il est possible d’étudier des versions plus simples (sous-problèmes) du problème original. Comme technique de décomposition par scénario, l’algorithme de recouvrement progressif est une des méthodes les plus populaires pour résoudre les problèmes de programmation stochastique multi-étapes. Malgré la décomposition complète par scénario, l’efficacité de la méthode du recouvrement progressif est très sensible à certains aspects pratiques, tels que le choix du paramètre de pénalisation et la manipulation du terme quadratique dans la fonction objectif du lagrangien augmenté. Pour le choix du paramètre de pénalisation, nous examinons quelques-unes des méthodes populaires, et nous proposons une nouvelle stratégie adaptive qui vise à mieux suivre le processus de l’algorithme. Des expériences numériques sur des exemples de problèmes stochastiques linéaires multi-étapes suggèrent que la plupart des techniques existantes peuvent présenter une convergence prématurée à une solution sous-optimale ou converger vers la solution optimale, mais avec un taux très lent. En revanche, la nouvelle stratégie paraît robuste et efficace. Elle a convergé vers l’optimalité dans toutes nos expériences et a été la plus rapide dans la plupart des cas. Pour la question de la manipulation du terme quadratique, nous faisons une revue des techniques existantes et nous proposons l’idée de remplacer le terme quadratique par un terme linéaire. Bien que qu’il nous reste encore à tester notre méthode, nous avons l’intuition qu’elle réduira certaines difficultés numériques et théoriques de la méthode de recouvrement progressif. / In the literature of optimization problems under uncertainty a common approach of dealing with two- and multi-stage problems is to use scenario analysis. To do so, the uncertainty of some data in the problem is modeled by stage specific random vectors with finite supports. Each realization is called a scenario. By using scenarios, it is possible to study smaller versions (subproblems) of the underlying problem. As a scenario decomposition technique, the progressive hedging algorithm is one of the most popular methods in multi-stage stochastic programming problems. In spite of full decomposition over scenarios, progressive hedging efficiency is greatly sensitive to some practical aspects, such as the choice of the penalty parameter and handling the quadratic term in the augmented Lagrangian objective function. For the choice of the penalty parameter, we review some of the popular methods, and design a novel adaptive strategy that aims to better follow the algorithm process. Numerical experiments on linear multistage stochastic test problems suggest that most of the existing techniques may exhibit premature convergence to a sub-optimal solution or converge to the optimal solution, but at a very slow rate. In contrast, the new strategy appears to be robust and efficient, converging to optimality in all our experiments and being the fastest in most of them. For the question of handling the quadratic term, we review some existing techniques and we suggest to replace the quadratic term with a linear one. Although this method has yet to be tested, we have the intuition that it will reduce some numerical and theoretical difficulties of progressive hedging in linear problems.