%0 Conference Proceedings %F ehmnst99 %A Eidorff, Peter Harry %A Henglein, Fritz %A Mossin, Christian %A Niss, Henning %A S\orensen, Morten Heine %A Tofte, Mads %T AnnoDomini: From type theory to Year 2000 conversion tool %B POPL '99: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages %P 1-14 %I ACM %C New York, NY, USA %X AnnoDomini is a source-to-source conversion tool for making COBOL programs Year 2000 compliant. It is technically and conceptually built upon type-theoretic techniques and methods: type-based specification, program analysis by type inference and type-directed transformation. These are combined into an integrated software reengineering tool and method for finding and fixing Year 2000 problems. AnnoDomini's primary goals have been \emph{flexibility} (support for multiple year representations), \emph{completeness} (identifying all potential Year 2000 problems), \emph{correctness} (correct fixes for Year 2000 problems) and a high degree of \emph{safe automation} in all phases (declarative specification of conversions, no second-guessing or dangerous heuristics). In this paper we present the type-theoretic foundations of AnnoDomini: type system, type inference, unification theory, semantic soundness, and correctness of conversion. We also describe how these foundations have been applied and extended to a common COBOL mainframe dialect, and how AnnoDomini is packaged with graphical user interface and syntax-sensitive editor into a commercially available software tool %U http://www.diku.dk/hjemmesider/ansatte/henglein/papers/eidorff1999.pdf %U http://doi.acm.org/10.1145/292540.292543 %8 January %D 1999