PL/SE Seminar: Making Programming Languages more Usable through Optimization
Speaker: Ross Tate, Cornell University
Date: Tuesday, December 11 2012
Time: 2:00PM to 3:30PM
Location: 32-G882 (reading room)
Host: Adam Chlipala, CSAIL
Contact: Adam Chlipala, firstname.lastname@example.orgRelevant URL: http://www.cs.cornell.edu/~ross/
Programming languages have long had to carefully balance between human usability and computational efficiency. Indeed, many programmers constantly need to keep efficiency in mind as they implement their projects. This concern often forces programmers to write code in ways that are hard for them and their colleagues to read but which will execute more efficiently. This may happen at fine-grained levels such as within a procedure, but it can even force programmers to use library designs that they know are fragile and error prone but which can get them the performance they need. In this presentation I will present technologies that enable programmers to extend the compiler with new optimizations by example and even to automatically infer optimizations from library properties. These technologies allow programmers to write intuitive code and execute efficient programs, thus making programming languages more usable by lifting the burden of optimization.
Bio: Ross Tate is an Assistant Professor at Cornell University, having recently graduated from the University of California, San Diego, where he was advised by Sorin Lerner. His research ranges over a wide area of programming languages and earned him the Microsoft Research Fellowship. Overarching his projects is a proclivity for solving problems in daily programming by pulling from theoretical domains such as category theory, logic, and semantics. In his work a UCSD, he developed new techniques for inferring program optimizations from simple language properties, and has since adapted those techniques to translation validators used to verify the correctness of optimizations and to enabling programmers to teach compilers new optimizations from simple examples. In his work at Microsoft Research, he designed algorithms for inferring memory safety of assembly code as part of a larger effort to build a verified operating system. In his work with Red Hat, he is helping design a type system with many object-oriented and functional features for their Ceylon programming language while still guaranteeing decidability by building off his solutions for Java's type system. In his work at Cornell, he formalized from first principles effect systems and their semantics, producing new insights on prior frameworks such as monads and identifying new opportunities for effects.
See other events happening in December 2012