Publications
The links below contain more than the usual pdf files; they contain an embedded video of the presentation and the powerpoint slides, for those people who would like a quick overview before reading the paper. They also have answers to common questions we have recieved.
- Transitioning from Structural to Nominal Code with Efficient Gradual Typing (OOPSLA 2021)
with Fabian Muehlboeck - Type Stability in Julia: Avoiding Performance Pathologies in JIT Compilation (OOPSLA 2021)
with Artem Pelenitsyn, Julia Belyakova, Benjamin Chung, and Jan Vitek - Evidenced Frames: A Unifying Framework Broadening Realizability Models (LICS 2021)
with Liron Cohen and Étienne Miquey - World Age in Julia: Optimizing Method Dispatch in the Presence of Eval (OOPSLA 2020)
with Julia Belyakova, Benjamin Chung, Jack Galinas, Jameson Nash, and Jan Vitek - First-Order Logic for Flow-Limited Authorization (CSF 2020) (Workshop Version: FCS 2019)
with Andrew K. Hirsch, Pedro H. Azevedo de Amorim, Ethan Cecchetti, and Owen Arden - The Effects of Effects on Constructivism (MFPS 2019)
with Liron Cohen and Sofia Abreu Faro - Empowering Union and Intersection Types with Integrated Subtyping (OOPSLA 2018)
with Fabian Muehlboeck - Strict and Lazy Semantics for Effects: Layering Monads and Comonads (ICFP 2018)
with Andrew K. Hirsch - Sound Gradual Typing is Nominally Alive and Well (OOPSLA 2017) (Distinguished Paper Award)
with Fabian Muehlboeck - Java and Scala's Type Systems are Unsound (OOPSLA 2016) (Distinguished Artifact Award)
with Nada Amin - Preventing Glitches and Short Circuits in High-Level Self-Timed Chip Specifications (PLDI 2015)
with Stephen Longfield, Brittany Nkounkou, and Rajit Manohar - Getting F-Bounded Polymorphism into Shape (PLDI 2014)
with Ben Greenman and Fabian Muehlboeck
and consultation from the Ceylon team at Red Hat - Mixed-Site Variance (FOOL 2013)
with consultation from the Kotlin team at JetBrains - The Sequential Semantics of Producer Effect Systems (POPL 2013)
- Taming Wildcards in Java's Type System (PLDI 2011)
with Alan Leung and Sorin Lerner - Inferable Object-Oriented Type Assembly Language (PLDI 2010)
with Juan Chen and Chris Hawblitzel - Generating Compiler Optimizations from Proofs (POPL 2010)
with Michael Stepp and Sorin Lerner - Equality Saturation: A New Approach to Optimization (POPL 2009, LMCS 2011, CAV 2011)
with Michael Stepp, Zachary Tatlock, and Sorin Lerner
Articles
- Java is Unsound: The Industry Perspective (2017)
featured by HackerNoon and dev.to
Kotlin
Due to my work on wildcards and Ceylon, I came into contact with the Kotlin team at JetBrains. They, too, are developing a next-generation object-oriented industry-scale programming language, and am acting primarily as a type-system advisor there as well. The two projects are very different, both in how they operate, and in what they are working towards. The contrast has been very educational, offering a diverse set of opinions on potential features or refinements, and resulting in subtle but important differences in the problems at hand. Most recently I have written a paper on a system I developed for Kotlin, which has a strong need to mix use-site and declaration-site variance together for purposes of compatibility and usability.
- Mixed-Site Variance (FOOL 2013)
Ceylon
Due to my work on wildcards, I came into contact with the Ceylon team at Red Hat. They were developing a next-generation object-oriented industry-scale programming language, attempting to incorporate all the experience offered by languages such as Java, C#, Scala, Smalltalk, and Python over the last decade or so. My role on the team was primarily as type-system advisor, making sure Ceylon's powerful features all work together cohesively.
- Getting F-Bounded Polymorphism into Shape (PLDI 2014)
with Ben Greenman and Fabian Muehlboeck - Empowering Union and Intersection Types with Integrated Subtyping (OOPSLA 2018)
with Fabian Muehlboeck - Lukas Eder: Top 10 Ceylon Language Features I Wish We Had in Java
Awards
- Distinguished Paper Award for Sound Gradual Typing is Nominally Alive and Well at OOPSLA 2017
- Junior Dahl-Nygaard Prize 2017
"Ross Tate has made fundamental contributions to type systems with applications to OO languages. This includes the discovery that although wildcards as in Java are undecidable in theory, programmers only use specific flavors of wildcards which keeps them decidable in practice (PLDI'11); similarly, he proposed that F-bounded polymorphism can be replaced by simpler concepts, which were sufficient for the use that programmers made of generics in a large corpus (PLDI'14). Finally, he discovered that Java wildcards and Scala path-dependent types, in combination with implicit null pointers, make the languages unsound (OOPSLA'16). In addition, he has had strong industrial impact via his involvement in the production languages Ceylon (Red Hat) and Kotlin (JetBrains)."
- Distinguished Artifact Award for Java and Scala's Type Systems are Unsound at OOPSLA 2016
- Microsoft Research Fellowship 2009
Students
Classes
CS-6117: Category Theory for Computer Scientists (Spring 2020)
CS-5152: Open-Source Software Engineering (Fall 2019)
CS-5152: Open-Source Software Engineering (Spring 2019)
CS-6117: Category Theory for Computer Scientists (Spring 2018)
CS-5152: Open-Source Software Engineering (Spring 2017)
CS-2110: OO Programming and Data Structures (Spring 2016)
CS-5152: Open-Source Software Engineering (Spring 2015)
CS-6117: Category Theory for Computer Scientists (Fall 2015)
CS-5152: Open-Source Software Engineering (Spring 2014)
CS-4120/4121/5120/5121: Introduction to Compilers (Fall 2014)
CS-5152: Open-Source Software Engineering (Spring 2013)
CS-6118: Types and Semantics (Fall 2013)
CSE-130: Programming Languages (Summer Session II 2010)
Research Internships
I interned under Daan Leijen at Microsoft Research in Redmond in Summer/Fall 2009. We designed a pure but effectful functional programming language, as well as a Hindley-Milner-like type inference algorithm with effects and higher-order polymorphism (based on Daan's HMF). In doing so, I improved compiler technology for inferring higher-ranked polymorphism. I also managed to generalize monads in order to formalize effect systems with multiple interacting effects.
I interned under Juan Chen and Chris Hawblitzel at Microsoft Research in Redmond in Summer/Fall 2008. I designed a type-inference algorithm for an x86 assembly type system for object-oriented programs, as can be seen at PLDI 2010. This typed assembly language, which we called iTalX, is now a key part of Microsoft Research's computer-verified memory-safe operating system, Verve. In order to design this inferable type system, I first designed a framework for existential types based on category theory, which has proven to be intuitive, powerful, and flexible. This framework was then reused for my work on Java's wildcards in PLDI 2011.
Industry Internships
I have interned at Treyarch, a studio of Activision, twice now. The first time I worked on the early stages of the Spider-Man 3 console game. The second time I worked on Spider-Man: Web of Shadows. My biggest contributions were in improving the scripting language used by the game designers, and this may have somewhat fostered my enjoyment of programming languages. I also worked a lot with computational geometry and corresponding graph theory.
Before that, I interned at CustomFlix. At the time, CustomFlix was a very small internet company which processed, distributed, and marketed personal videos. I held various roles such as architect, tester, lead, and web developer.
Post Script
I stole this page from Patrick "Maxim" Rondon.
I found my grandpa online. Thought it was pretty cool.