Research Projects

Web Security

• ADsafety shows how to verify language-based Web sandboxes.
• Microsoft IBEX allows programmers to write verifiably secure Web browser extensions.
• Google Belay demonstrates password-free login and fine-grained sharing on the Web.

JavaScript

• λ_JS is a tested core calculus for JavaScript.
• Strobe is a JavaScript type-checker that integrates program analysis in a modular way.

Programming Networks

• PANE allows network administrators to define security policies that allow end-users to reconfigure software-defined networks.
• Frenetic is a high-level language for programming software-defined networks.

Functional-Reactive Programming

• Flapjax is a functional-reactive programming language for Web applications.