Programming and Verifying the Interactive Web
Server-side Web applications have grown increasingly common, sometimes even replacing brick and mortar as the principal interface of corporations. Correspondingly, Web browsers grow ever more powerful, empowering users to attach bookmarks, switch between pages, clone windows, and so forth. As a result, Web interactions are not straight-line dialogs but complex nets of interaction steps.
In practice, programmers are unaware of or are unable to handle these nets of interaction, making the Web interfaces of even major organizations buggy and thus unreliable. Even when programmers do address these constraints, the resulting programs have a seemingly mangled structure, making them difficult to develop and hard to maintain.
In this talk, I will describe these interactions and then show how programming language ideas can shed light on the resulting problems and present solutions at various levels. I will also describe some challenges these programs pose to computer-aided verification, and outline solutions to these problems.
Shriram Krishnamurthi is an Assistant Professor of Computer Science at Brown University. His research lies at the confluence of programming languages, software engineering and computer-aided verification. His recent work has focused on the semantics, verification, and use of new forms of software composition and interaction. He is a co-author of the DrScheme programming environment, the FASTLINK genetic linkage analysis package, the Continue conference paper server, and the book How to Design Programs (MIT Press, 2001). He has more recently written the text Programming Languages: Application and Interpretation. He also coordinates the TeachScheme! high school computer science outreach program.