Jeremy Siek is an Associate 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, Jeremy invented the gradual typing approach to mixing static and dynamic type checking within the same language. Prior to that, Jeremy authored the Boost Graph Library and attempted to add concepts to C++. Jeremy is a member of the Programming Languages Group at IU and the Center for Research in Extreme Scale Technologies (CREST).

Email:, Office: LH 330C, Blog, Twitter, CV


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.
  • Microsoft created a gradually-typed dialect of JavaScript, called TypeScript.
  • The implicits feature of Scala was inspired by my work on concepts for C++.

Recent Papers and Talks

The full list is available on Google Scholar and DBLP.

  • Monotonic References for Gradual Typing with Michael M. Vitousek, Matteo Cimini, Sam Tobin-Hochstadt, and Ronald Garcia. Draft, July 2014. pdf  Isabelle (Supersedes the arxiv draft and now includes blame tracking!)
  • Design and Evaluation of Gradual Typing for Python with Michael M. Vitousek, Andrew Kent, and Jim Baker. Updated Draft, June 2014. pdf
  • A Mechanized Semantics for System F via the F Machine (slides from IU Logic Seminar) pdf
  • Meta-tracing makes a fast Racket with Carl Friedrich Bolz, Tobias Pape, and Sam Tobin-Hochstadt. In Dyla’14, June 2014. pdf
  • Blame, coercions, and threesomes, precisely with Peter Thiemann and Philip Wadler. Draft, March 2014. pdf
  • Monotonic References for Gradual Typing with Vitousek, includes proof of type safety mechanized in Isabelle arxiv
  • Compile-time Reflection and Metaprogramming for Java with Weiyu Miao. In PEPM 2014. pdf
  • Linking isn’t Substitution (slides from talk at HOPE 2013) pdf
  • Interpretations of the Gradually-Typed Lambda Calculus with  Garcia. In Scheme and Functional Programming 2012. pdf
  • Reliable Generation of High-Performance Matrix Algebra with Nelson, Belter, Jessup, and Norris. Submitted to ACM TOMS. pdf
  • Modular Type-Safety Proofs in Agda with Schwaab. In PLPV 2013. pdf
  • Well-typed Islands Parse Faster with Silkensen. In TFP 2012. pdf


Previous courses at Univ. of Colorado:


  1. Weiyu Miao (Generic Programming, Metaprogramming)
  2. John Michalakes (High-Performance Computing for Wind Energy Research)
  3. Thomas Nelson (Optimization of linear algebra kernels)
  4. Michael M. Vitousek (Gradual Python)
  5. Chris Wailes (Chapel and Parallel Programming Languages)


  1. Geoffrey Belter (Apple)
    Ph.D. thesis: Efficient Generation of Sequences of Dense Linear Algebra through Auto-Tuning
  2. Shashank Bharadwaj (VMware)
  3. Jonathan Turner (Microsoft)
  4. Erik Silkensen (Ph.D. student at Northeastern Univ.)
  5. Neelam Agrawal (National Instruments)
  6. Sri Teja Basava (National Instruments)
  7. Ian Karlin (Postdoc at Lawrence Livermore National Laboratory)
  8. Justin Gottschlich (Intel Research Labs)
    Ph.D. thesis: Invalidating Transactions: Optimizations, Theory, Guarantees, and Unification
  9. Moss Prescott (Terma Software Labs)
    M.S. thesis: Speaking for the Trees: a New (Old) Approach to Languages and Syntax
  10. Christopher Schwaab (Ph.D. student at the Univ. of St. Andrews)
  11. David Broman (Post-doc at UC Berkeley)
    Ph.D. thesis: Meta-Languages and Semantics for Equation-Based Modeling and Simulation