In this talk we explain what the Year 2000 problem is and show its close connection to type theory. We present a new type discipline which allows users to find and correct Year 2000 problems in COBOL programs. The type discipline is implemented in a tool called AnnoDomini, which is sold as a commercial product for remediation of IBM OS/VS COBOL programs. Although developed specifically for business applications, AnnoDomini borrows heavily from research in programming languages. AnnoDomini is written in Standard ML, it provides users with abstract (year) types, it is implemented using unification-based type inference, it was specified using operational semantics, and the core of its design was guided by formulating and proving theorems.
The talk presents the basic ideas of AnnoDomini and ends with a demo.