Sam Tobin-Hochstadt
The most important decisions a scholar makes are what problems to work on. - James Tobin
Associate Professor
PLT &
PL @
Department of Computer Science
Indiana University
Office: Luddy Hall, Room 3022
Email: samth@iu.edu
Microblogging: @samth, @samth.bsky.social
Curriculum Vitae: pdf
Papers: DBLP, Google Scholar, arXiv, ACM
Software: GitHub
News
I'm looking for new Ph.D students at Indiana University Computer Science, please email me if you are interested.
New paper: Garbage Collection for Mostly Serialized Heaps with Chaitanya S. Koparkar and Ryan Newton; appeared at ISMM 2024
New paper: Rhombus: A New Spin on Macros without All the Parentheses with Matthew Flatt and others; appeared at OOPSLA 2023
New papers: Sham: A DSL for Fast DSLs with Rajan Walia and Chung-chieh Shan and Type Checking Extracted Methods with Yuquan Fu; both appeared in Art, Science, and Engineering of Programming 2022
New paper: Forward build systems, formally with Sarah Spall and Neil Mitchell; appeared at CPP 2022
New paper: Corpse reviver: sound and efficient gradual typing via contract verification with Cameron Moy, Phuc C. Nguyen, and David Van Horn; appeared at POPL 2021
Our recent work includes advances in gradual typing, domain-specific languages, JIT compilers, and program verifiers, among other areas of PL design and implementation.
Research Projects
My research focuses on the design and implementation of programming systems. I'm particularly interested in programming languages that support the evolution of software. I primarily work on Racket and Typed Racket as well as with Mozilla Research on JavaScript.
Typed Racket
I created and maintain Typed Racket, a statically-typed dialect of Racket that allows existing untyped Racket programs to be enriched with types.
Papers
Type Checking Extracted Methods.
With Yuquan Fu.
Art, Science, and Engineering of Programming, 2022.
[
Journal | arXiv
]
Corpse reviver: sound and efficient gradual typing via contract verification.
With Cameron Moy, Phuc C. Nguyen and David Van Horn.
Symposium on Principles of Programming Languages (POPL), January 2021.
[
ACM | arXiv
]
Sound gradual typing: only mostly dead.
With Spenser Bauman, Carl Friedrich Bolz and Jeremy G. Siek.
Object Oriented Programming, Systems, Languages and Applications (OOPSLA), October 2017.
[
ACM
]
Migratory Typing: Ten Years Later.
With Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, Ben Greenman, Andrew M. Kent, Vincent St-Amour, T. Stephen Strickland and Asumu Takikawa.
Summit on Advances in Programming Languages (SNAPL), May 2017.
[
ACM
]
Occurrence typing modulo theories.
With Andrew M. Kent and David Kempe.
Conference on Programming Language Design and Implementation (PLDI), June 2016.
[
ACM
]
Practical Optional Types for Clojure.
With Ambrose Bonnaire-Sergeant and Rowan Davies.
European Symposium on Programming (ESOP), April 2016.
[
Springer
]
The Recursive Union of Some Gradual Types.
With Jeremy G. Siek.
A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler, 2016.
[
Springer
]
Towards Practical Gradual Typing.
With Asumu Takikawa, Daniel Feltey, Earl Dean, Matthew Flatt, Robert Bruce Findler and Matthias Felleisen.
European Conference on Object-Oriented Programming (ECOOP), July 2015.
[
PDF | Artifact | Documentation
]
Monotonic References for Efficient Gradual Typing.
With Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini and Ronald Garcia.
European Symposium on Programming (ESOP), April 2015.
[
PDF
]
Constraining Delimited Control with Contracts.
With Asumu Takikawa and T. Stephen Strickland.
European Symposium on Programming (ESOP), March 2013.
[
PDF
]
Gradual Typing for First-class Classes.
With Asumu Takikawa, T. Stephen Strickland, Christos Dimoulas and Matthias Felleisen.
Object Oriented Programming, Systems, Languages and Applications (OOPSLA), October 2012.
[
PDF
]
Proceedings of the Third Workshop on Script to Program Evolution.
NU CCIS Technical Report NU-CCIS-12-02, June 2012.
[
PDF
]
Complete Monitors for Behavioral Contracts.
With Christos Dimoulas and Matthias Felleisen.
European Symposium on Programming (ESOP), March 2012.
[
PDF
]
Typing the Numeric Tower.
With Vincent St-Amour, Matthew Flatt and Matthias Felleisen.
Symposium on Practical Aspects of Declarative Languages (PADL), January 2012.
[
PDF
]
Logical Types for Untyped Languages.
With Matthias Felleisen.
International Conference on Functional Programming (ICFP), September 2010.
[
PDF | ACM DL
]
The Design and Implementation of Typed Scheme (Preprint).
With Matthias Felleisen.
Accepted for publication in Higher-Order and Symbolic Computation, September 2010.
[
PDF | arXiv
]
Functional Data Structures for Typed Racket.
With Hari Prashanth K R.
Workshop on Scheme and Functional Programming, August 2010.
[
PDF | PLaneT Package
]
Typed Scheme: From Scripts to Programs.
PhD Dissertation, Northeastern University, January 2010.
[
PDF
]
Cycles without pollution: a gradual typing poem.
With Robert Bruce Findler.
1st International Workshop on Script to Program Evolution (STOP), July 2009.
[
PDF | ACM DL
]
Practical Variable-Arity Polymorphism.
With T. Stephen Strickland and Matthias Felleisen.
European Symposium on Programming (ESOP), March 2009.
[
PDF | Springer
]
The Design and Implementation of Typed Scheme.
With Matthias Felleisen.
Symposium on Principles of Programming Languages (POPL), January 2008.
[
PDF | ACM DL | Formal Models
]
Interlanguage Migration: From Scripts to Programs.
With Matthias Felleisen.
Dynamic Languages Symposium (DLS), October 2006.
[
PDF | ACM DL
]
Talks
Evolving Software From Scripts to Programs, ETH Zurich Department of Computer Science, Zurich, CH, April, 2013.
Evolving Software From Scripts to Programs, Indiana University Department of Computer Science, Bloomington, IN, March, 2013.
Evolving Software From Scripts to Programs, Iowa State University Software Engineering Seminar, Ames, IA, March, 2013.
Evolving Software From Scripts to Programs, University of Idaho Department of Computer Science, Moscow, ID, March, 2013.
Occurrence Typing, Dagstuhl meeting on Foundations of Scripting Languages, Wadern, Germany, January, 2012.
Growing Software: From Scripts to Programs, Oregon State University EECS Colloquium, Corvallis, Oregon, March 2011.
From Scripts to Programs, Indiana University Department of Computer Science, Bloomington, IN, November 2010.
Logical Types for Untyped Languages, International Conference on Functional Programming, Baltimore, MD, September 2010.
Logical Types for Scheme, New England Programming Languages and Systems Symposium, Yale University, April 2010.
Typed Scheme: From Scripts to Programs, Harvard University, Cambridge, MA, February 2010.
Types for Scheme, in Scheme, Boston Lisp Meeting, Boston, MA, December 2009.
Typed Scheme: From Scripts to Programs, Dissertation Defense, Northeastern University, Boston, MA, December 2009.
Typed Scheme: From Scripts to Programs, Sun Microsystems Laboratories, Burlington, MA, September 2009.
The Design and Implementation of Typed Scheme, Symposium in Honor of Mitchell Wand, Boston, MA, August 2009.
Cycles without pollution: a gradual typing poem, 1st International Workshop on Script to Program Evolution, Genoa, Italy, July 2009.
To Type or Not To Type, Northeastern University ACM Speaker Series, Boston, MA, April 2008.
Typed Scheme, Northeastern University CCIS Open House, Boston, MA, March 2008.
The Design and Implementation of Typed Scheme, Symposium on Principles of Programming Languages (POPL), San Fransisco, CA, January 2008.
Types for Untyped Languages, Northeastern University CCIS Open House, Boston, MA, March 2007.
Interlanguage Migration: From Scripts to Programs, Dynamic Languages Symposium (DLS), Portland, OR, October 2006.
Domain-Specific Languages
I develop techniques and tools for creating efficient domain-specific languages, particularly for high-performance computing and probabilistic programming. Additionally, developing Racket, I have helped to build a programmable programming language that allows developers to create custom languages for everything from pattern matching to type checking.
Papers
Rhombus: A New Spin on Macros without All the Parentheses.
With Matthew Flatt, Taylor Allred, Nia Angle, Stephen De Gabrielle, Robert Bruce Findler, Jack Firth, Kiran Gopinathan, Ben Greenman, Siddhartha Kasivajhula, Alex Knauth, Jay McCarthy, Sam Phillips, Sorawee Porncharoenwase and Jens Axel Søgaard.
Object Oriented Programming, Systems, Languages and Applications (OOPSLA), October 2023.
[
ACM
]
Sham: A DSL for Fast DSLs.
With Rajan Walia and Chung-chieh Shan.
Art, Science, and Engineering of Programming, 2022.
[
Journal | arXiv
]
From high-level inference algorithms to efficient code.
With Rajan Walia, Praveen Narayanan, Jacques Carette and Chung-chieh Shan.
International Conference on Functional Programming (ICFP), August 2019.
[
ACM
]
Rebuilding racket on chez scheme (experience report).
With Matthew Flatt, Caner Derici, R. Kent Dybvig, Andrew W. Keep, Gustavo E. Massaccesi, Sarah Spall and Jon Zeppieri.
International Conference on Functional Programming (ICFP), August 2019.
[
ACM
]
A programmable programming language.
With Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, Shriram Krishnamurthi, Eli Barzilay and Jay McCarthy.
Communications of the ACM, March 2018.
[
ACM
]
Compiling Tree Transforms to Operate on Packed Representations.
With Michael Vollmer, Sarah Spall, Buddhika Chamith, Laith Sakka, Chaitanya S. Koparkar, Milind Kulkarni and Ryan Newton.
European Conference on Object-Oriented Programming (ECOOP), June 2017.
[
ACM
]
The Racket Manifesto.
With Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, Shriram Krishnamurthi, Eli Barzilay and Jay McCarthy.
Summit on Advances in Programming Languages (SNAPL), May 2015.
[
PDF | HTML
]
Meta-tracing makes a fast Racket.
With Carl Friedrich Bolz, Tobias Pape and Jeremy G. Siek.
Workshop on Dynamic Languages and Applications (DYLA), June 2014.
[
PDF | GitHub
]
Taming the Parallel Effect Zoo: Extensible Deterministic Parallelism with LVish.
With Lindsey Kuper, Aaron Todd and Ryan Newton.
Conference on Programming Languages Design and Implementation (PLDI), June 2014.
[
PDF | LVish
]
The Network as a Language Construct.
With Tony Garnock-Jones and Matthias Felleisen.
European Symposium on Programming (ESOP), April 2014.
[
PDF | Web Page | Marketplace
]
Chaperones and Impersonators: Runtime support for reasonable interposition.
With T. Stephen Strickland, Robert Bruce Findler and Matthew Flatt.
Object Oriented Programming, Systems, Languages and Applications (OOPSLA), October 2012.
[
PDF | Web Page | Documentation
]
Optimization Coaching.
With Vincent St-Amour and Matthias Felleisen.
Object Oriented Programming, Systems, Languages and Applications (OOPSLA), October 2012.
[
PDF | GitHub
]
Run Your Research: On the Effectiveness of Lightweight Mechanization.
With Casey Klein, John Clements, Christos Dimoulas, Carl Eastlund, Matthias Felleisen, Matthew Flatt, Jay McCarthy, Jon Rafkind and Robert Bruce Findler.
Symposium on Principles of Programming Languages (POPL), January 2012.
[
PDF | Models | Redex
]
Languages as Libraries.
With Vincent St-Amour, Ryan Culpepper, Matthew Flatt and Matthias Felleisen.
Conference on Programming Language Design and Implementation (PLDI), June 2011.
[
PDF | ACM DL
]
Extensible Pattern Matching in an Extensible Language (Preprint).
October 2010.
[
PDF | arXiv | Documentation
]
Extensible Pattern Matching in an Extensible Language (Abstract).
Symposium on Implementation and Application of Functional Languages, September 2010.
[
PDF | Utrecht Technical Report
]
Where are you going with those types? (Abstract).
With Vincent St-Amour, Matthew Flatt and Matthias Felleisen.
Symposium on Implementation and Application of Functional Languages, September 2010.
[
PDF | Utrecht Technical Report
]
Advanced Macrology and the Implementation of Typed Scheme.
With Ryan Culpepper and Matthew Flatt.
Workshop on Scheme and Functional Programming, September 2007.
[
PDF | Proceedings
]
Analysis and Verification
I am developing analysis and verification techniques for modular programs with rich specifications.
Papers
Size-change termination as a contract: dynamically and statically enforcing termination for higher-order programs.
With Phuc C. Nguyen, Thomas Gilray and David Van Horn.
Conference on Programming Language Design and Implementation (PLDI), June 2019.
[
ACM
]
Soft contract verification for higher-order stateful programs.
With Phuc C. Nguyen, Thomas Gilray and David Van Horn.
Symposium on Principles of Programming Languages (POPL), January 2018.
[
ACM
]
Higher order symbolic execution for contract verification and refutation.
With Phuc C. Nguyen and David Van Horn.
Journal of Functional Programming, 2017.
[
Cambridge
]
Soft Contract Verification.
With Phil Nguyen and David Van Horn.
International Conference on Functional Programming (ICFP), September 2014.
[
ACM | arXiv
]
Higher-order Symbolic Execution via Contracts.
With David Van Horn.
Object Oriented Programming, Systems, Languages and Applications (OOPSLA), October 2012.
[
PDF | arXiv
]
Semantic Solutions to Program Analysis Problems.
With David Van Horn.
Fun Ideas and Thoughts Session at the Conference on Programming Language Design and Implementation, June 2011.
[
PDF | arXiv
]
Systems and Performance
I work on garbage collection, memory management, and performance optimization for functional languages and parallel systems. I also work on formal foundations and practical implementations of build systems, focusing on correct dependency tracking and efficient incremental builds.
Papers
Garbage Collection for Mostly Serialized Heaps.
With Chaitanya S. Koparkar, Vidush Singhal, Aditya Gupta, Mike Rainey, Michael Vollmer, Artem Pelenitsyn, Milind Kulkarni and Ryan Newton.
International Symposium on Memory Management (ISMM), June 2024.
[
ACM
]
Forward build systems, formally.
With Sarah Spall and Neil Mitchell.
Certified Programs and Proofs (CPP), January 2022.
[
ACM | arXiv
]
Build scripts with perfect dependencies.
With Sarah Spall and Neil Mitchell.
Object Oriented Programming, Systems, Languages and Applications (OOPSLA), November 2020.
[
ACM | arXiv
]
Parallel type-checking with haskell using saturating LVars and stream generators.
With Ryan Newton, Ömer S. Ağacan and Peter P. Fogg.
Symposium on Principles and Practice of Parallel Programming (PPoPP), March 2016.
[
ACM
]
Industry Collaboration
I have collaborated with industry partners on programming language design and implementation. In collaboration with Mozilla Research and ECMA Technical Committee 39, I worked on the next version of the JavaScript language, focusing on making JavaScript an effective language for building large-scale web applications. I also worked with Sun Labs Programming Language Research Group to develop Fortress, a new language for high-performance, multicore and scientific computing.
Papers
Modules for JavaScript (Preprint).
With Dave Herman.
April 2011.
[
PDF
]
The Fortress Language Specification.
With Eric Allen, David Chase, Joe Hallett, Victor Luchangco, Jan-Willem Maessen, Sukyoung Ryu and Guy Steele.
Sun Microsystems Technical Report, Version 1.0, 2008.
[
PDF
]
A Core Calculus of Metaclasses.
With Eric Allen.
Workshop on Foundations of Object-Oriented Languages (FOOL), January 2005.
[
PDF | Proceedings
]
JavaScript Proposals
Modules and
Module Loaders.
With Dave Herman.
Drafts from September 2011.
Private Names.
With Dave Herman and Allen Wirfs-Brock.
Draft from September 2011.
Talks
Research meets Application: Life on the EcmaScript Committee, Northeastern University Ph.D. Seminar, Boston, MA, 2012.
The Future of the Web: It's coming!, Childrens Hospital developers group, Boston, MA, December 2011.
Activities
- PLDI 2015, Program Committee
- IFL 2014, Chair
- POPL 2015, External Review Committee
- DLS 2014, Program Committee
- ICFP Student Research Competition 2014, Program Committee
- OOPSLA 2013, Program Committee
- ICFP 2012, Program Committee
- STOP 2012, Chair
- Scheme Workshop 2011, Program Committee
- NEPLS 25, Chair
- TLDI 2011, Program Committee
- FOOL 2010, Program Committee
- TFP 2010, Program Committee
Teaching
I regularly teach graduate and undergraduate courses in programming languages, especially C211 (Introduction to Computer Science).
Papers
From Principles to Practice with Class in the First Year.
With David Van Horn.
Trends in Functional Programming in Education, May 2013.
[
PDF
]
Personal
In the rest of my life, I play Ultimate and I go outside.
My wife, Katie Edmonds, is a Scientist in the IU Chemistry Department.