Jeremy Siek is a Professor of Computer Science in the School of Informatics and Computing at Indiana University. Jeremy teaches courses in programming, programming languages, compilers, logic, and other areas of computer science. Jeremy designs new language features to help programmers create and use software libraries and domain-specific languages, especially generic and high-performance ones. In particular, with Walid Taha, Jeremy invented the gradual typing approach to mixing static and dynamic type checking within the same language. Prior to that, Jeremy co-authored the Boost Graph Library and attempted to add concepts to C++. Jeremy is a member of the Center for Programming Systems at IU and Jeremy is an Advocate for gender equity.
I’ve been fortunate to see some of my ideas get used in the software industry:
- Facebook has added gradual typing to PHP. See the article in Wired magazine.
- The implicits feature of Scala was inspired by my work on concepts for C++.
My group’s research is currently funded by the following sponsors.
- The National Science Foundation awarded the following projects:
- Facebook is supporting us through a Faculty Research Award.
Recent Papers and Talks
- Toward a Mechanized Encyclopedia of Gradual Typing. Talk at University of Chile. July 2019. slides
- Transitivity of Subtyping for Intersection Types. Draft Paper. June 2019. agda arXiv
- Toward Efficient Gradual Typing. Talk at INRIA Gallium. February 21, 2019. slides
- Toward Efficient Gradual Typing for Structural Types via Coercions, Andre Kuhlenschmidt, Deyaaeldeen Almahallawi, and Jeremy G. Siek. PLDI 2019. pdf. This is an updated version of the below arXiv draft. It adds new performance results but narrows the paper by removing monotonic references.
- Gradual typing: a new perspective
Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani, Jeremy G. Siek
Proceedings of the ACM on Programming Languages, 2019.
- The State of the Art in Gradual Typing,
Talk at the CS Colloquium, Indiana University. slides
- Intersection Types, Sub-formula Property, and the Functional Character of the Lambda Calculus, Talk at IU CPS Meeting slides.
- Crash Course on Notation in Programming Language Theory at LambdaConf 2018. slides video part 1 and part 2
- Modeling the Functional Character of the Lambda Calculus,
Jeremy G. Siek. Isabelle document available here. Also see this
- Efficient Gradual Typing, Andre Kuhlenschmidt, Deyaaeldeen Almahallawi, and Jeremy G. Siek. Pre-print on arXiv.
- Back to the Future with Denotational Semantics.
Talk at Off the Beaten Track, Jan. 2018. slides.
- Revisiting Elementary Denotational Semantics. Available on arXiv and in submission, Isabelle mechanization.
- B629: Topics in PL: Denotational Semantics Spring 2018
- C343/H343: Data Structures Fall 2019, Fall 2017, Fall 2016, Fall 2015, Fall 2014, Fall 2013
- P423/P523: Compilers (aka. Programming Language Implementation) Fall 2018, Spring 2016, Spring 2014
- B522: Programming Language Foundations Spring 2015
- C++, Short and Sweet, an Online C++ Course for Beginners at Udemy.
Previous courses at Univ. of Colorado:
- Fall 2012: Compiler Construction
- Fall 2011: Fundamentals of Programming Languages
- Fall 2011: Discrete Mathematics for Computer Engineers
- Spring 2011: Discrete Mathematics for Computer Engineers
- Spring 2011: Theorem Proving in Isabelle
- Fall 2010: Compiler Construction
Information for Students at IU
- How do I deal with being on a waitlist during course registration?
- What are the requirements for a CS MS degree?
- What are the requirements for a CS PhD degree?
Students and Post-Doc’s
- Andre Kuhlenschmidt (Ph.D. student, Compilation of Gradually Typed Languages)
- Deyaaeldeen Almahallawi (Ph.D. student, Compilation of Gradually Typed Languages)
- Matthew Heimerdinger (Ph.D. student, Denotational semantics and proofs of compiler correctness)
- Michael M. Vitousek (Facebook, Ph.D. thesis: Gradual Typing for Python, Unguarded)
- Chris Wailes (Google, Parallel Programming Languages)
- Matteo Cimini (Assistant Professor, Univ. of Massachusetts Lowell)
- Spenser Bauman (Ph.D. student, Meta-tracing JIT for Racket)
- Di Zhong (Undergraduate Research, now Ph.D. student at Northeastern Univ.)
- Zeina Migeed (Research co-op from Northeastern, now Ph.D. student at UCLA)
- Steev Young (Undergraduate Research in Gradual Typing)
- Josie Bealle (Summer Research Opportunity in Computing)
- Andre Yuri (Summer Research Opportunity in Computing)
- Weiyu Miao (LinkedIn)
Ph.D. thesis: Reflective Metaprogramming
- Geoffrey Belter (Apple)
Ph.D. thesis: Efficient Generation of Sequences of Dense Linear Algebra through Auto-Tuning
- Shashank Bharadwaj (VMware)
- Jonathan Turner (Microsoft Typescript => Mozilla Rust)
- Erik Silkensen (Flatiron Solutions)
- Neelam Agrawal (National Instruments)
- Sri Teja Basava (National Instruments)
- Ian Karlin (Postdoc at Lawrence Livermore National Laboratory)
- Justin Gottschlich (Parallel Computing Lab @ Intel Labs)
Ph.D. thesis: Invalidating Transactions: Optimizations, Theory, Guarantees, and Unification
- Moss Prescott (SlamData)
M.S. thesis: Speaking for the Trees: a New (Old) Approach to Languages and Syntax
- Christopher Schwaab (Ph.D. student at the Univ. of St. Andrews)
- David Broman (Assoc. Prof. at KTH Royal Inst. of Tech., Sweden)
Ph.D. thesis: Meta-Languages and Semantics for Equation-Based Modeling and Simulation
Authorizor (Free) Links to ACM Publications
- Sound gradual typing: only mostly dead
Spenser Bauman, Carl Friedrich Bolz-Tereick, Jeremy Siek, Sam Tobin-Hochstadt
Proceedings of the ACM on Programming Languages, 2017.
- Gradually typed symbolic expressions
- Theorems for free for free: parametricity, with and without types
- Big types in little runtime: open-world soundness and collaborative blame for gradual type systems
- Automatically generating the dynamic semantics of gradually typed languages
- The gradualizer: a methodology and algorithm for generating gradual type systems
- Pycket: a tracing JIT for a functional language
- Blame and coercion: together again for the first time
- Reliable Generation of High-Performance Matrix Algebra
- Design and evaluation of gradual typing for python
- Interpretations of the gradually-typed lambda calculus
- Blame for all
- Threesomes, with and without blame
- Gradual typing with unification-based inference
- Concepts: linguistic support for generic programming in C++
- Essential language support for generic programming
- A comparative study of language support for generic programming
- The generic graph component library