Inferable object-oriented typed assembly language. - Ross Tate; Juan Chen; Chris Hawblitzel (PLDI, 2010)

Generating compiler optimizations from proofs. - Ross Tate; Michael Stepp; Sorin Lerner (POPL, 2010)

Equality-Based Translation Validator for LLVM. - Michael Stepp; Ross Tate; Sorin Lerner (CAV, 2011)

Taming wildcards in Java's type system. - Ross Tate; Alan Leung; Sorin Lerner (PLDI, 2011)

Equality Saturation: A New Approach to Optimization - Ross Tate; Michael Stepp; Zachary Tatlock; Sorin Lerner (Log. Methods Comput. Sci., 2011)

Equality saturation: using equational reasoning to optimize imperative functions. - Ross Tate (2012)

The sequential semantics of producer effect systems. - Ross Tate (POPL, 2013)

Getting F-bounded polymorphism into shape. - Ben Greenman; Fabian Muehlboeck; Ross Tate (PLDI, 2014)

Preventing glitches and short circuits in high-level self-timed chip specifications. - Stephen Longfield Jr.; Brittany Nkounkou; Rajit Manohar; Ross Tate (PLDI, 2015)

Java and scala's type systems are unsound: the existential crisis of null pointers. - Nada Amin; Ross Tate (OOPSLA, 2016)

Retargeting Gradual Typing (Invited Talk). - Ross Tate (ECOOP, 2017)

Sound gradual typing is nominally alive and well. - Fabian Muehlboeck; Ross Tate (Proc. ACM Program. Lang., 2017)

Strict and lazy semantics for effects: layering monads and comonads. - Andrew K. Hirsch; Ross Tate (Proc. ACM Program. Lang., 2018)

Empowering union and intersection types with integrated subtyping. - Fabian Muehlboeck; Ross Tate (Proc. ACM Program. Lang., 2018)

The Effects of Effects on Constructivism. - Liron Cohen 001; Sofia Abreu Faro; Ross Tate (MFPS, 2019)

First-Order Logic for Flow-Limited Authorization. - Andrew K. Hirsch; Pedro H. Azevedo de Amorim; Ethan Cecchetti; Ross Tate; Owen Arden (CSF, 2020)

World Age in Julia: Optimizing Method Dispatch in the Presence of Eval (Extended Version). - Julia Belyakova; Benjamin Chung; Jack Gelinas; Jameson Nash; Ross Tate; Jan Vitek (CoRR, 2020)

World age in Julia: optimizing method dispatch in the presence of eval. - Julia Belyakova; Benjamin Chung; Jack Gelinas; Jameson Nash; Ross Tate; Jan Vitek (Proc. ACM Program. Lang., 2020)

Evidenced Frames: A Unifying Framework Broadening Realizability Models. - Liron Cohen 001; Étienne Miquey; Ross Tate (LICS, 2021)

Type Stability in Julia: Avoiding Performance Pathologies in JIT Compilation (Extended Version). - Artem Pelenitsyn; Julia Belyakova; Benjamin Chung; Ross Tate; Jan Vitek (CoRR, 2021)

Transitioning from structural to nominal code with efficient gradual typing. - Fabian Muehlboeck; Ross Tate (Proc. ACM Program. Lang., 2021)

Type stability in Julia: avoiding performance pathologies in JIT compilation. - Artem Pelenitsyn; Julia Belyakova; Benjamin Chung; Ross Tate; Jan Vitek (Proc. ACM Program. Lang., 2021)

Type Stability in Julia: Avoiding Performance Pathologies in JIT Compilation (Artifact). - Artem Pelenitsyn; Julia Belyakova; Benjamin Chung; Ross Tate; Jan Vitek (Zenodo, 2021)

Decidable Subtyping of Existential Types for Julia. - Julia Belyakova; Benjamin Chung; Ross Tate; Jan Vitek (Proc. ACM Program. Lang., 2024)