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.

Office: Luddy Hall 3016, Blog, github, Twitter, CV, Mastadon: @jeremysiek@types.pl

Deduce Proof Assistant

The Deduce proof assistant is an educational tool that helps students to develop correct code. You can read about it on the web page for Deduce and from a series of blog posts that I have been writing.

Phishing Scam: Research Assistant Position

There is an ongoing email phishing scam that is using my name. If you receive an email offering you a job without first meeting with me in person, please report it to phishing@iu.edu. Please do not send me email to check whether it is legitimate. Thank you.

Books

  • Essentials of Compilation (Racket version: pdf and available from MIT Press, Python version: pdf and also available from MIT Press)
  • The Boost Graph Library (ebook from Pearson, print from Amazon)

Technology Transfer

I’ve been fortunate to see some of my ideas get used in the software industry:

  • Microsoft created a gradually-typed dialect of JavaScript, called TypeScript.
  • Facebook has added gradual typing to PHP. See the article in Wired magazine.
    Facebook has also created Flow, a static type checker for JavaScript.

Recent Papers and Talks

The full list is available on Google Scholar and DBLP. Also, see further below for “authorizer” links to my ACM publications.

  • Quest Complete: the Holy Grail of Gradual Security. Tianyu Chen and Jeremy G. Siek. Accepted for publication at PLDI 2024. Draft on arXiv.
  • An Introduction to Step-indexed Logical Relations via Type Safety for STLC + fix. Jeremy G. Siek. IU PL Wonks, November 2023. video and slides
  • Mechanized Noninterference for Gradual Security. Tianyu Chen and Jeremy G. Siek. Draft on arXiv. November 2022.
  • Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi. Jeremy G. Siek and Tianyu Chen. Article in Journal of Functional Programming. November 2021.
  • Blame and coercion: Together again for the first time. Jeremy G. Siek, Peter Thiemann, and Philip Wadler. Article in the Journal of Functional Programming. October 2021.
  • Filter Models for Compiler Correctness. Invited Talk at the workshop on Intersection Types and Related Systems (ITRS) 2021. video and slides.

Teaching

Previous courses at Univ. of Colorado:

Information for Students at IU

Students

  1. Tianyu Chen (Ph.D. student, Gradual information flow types for security)

Alumni

  1. Andre Kuhlenschmidt (Meta, Software Engineer)
  2. Matthew Heimerdinger (Two Six Technologies, Research Scientist)
  3. Deyaaeldeen Almahallawi (Microsoft, Senior Software Engineer, Ph.D. thesis: Towards Efficient Gradual Typing via Monotonic References and Coercions)
  4. Kuang-Chen Lu (Brown Univ., M.S. thesis: Equivalence of Cast Representations in Gradual Typing)
  5. Michael M. Vitousek (Facebook, Ph.D. thesis: Gradual Typing for Python, Unguarded)
  6. Chris Wailes (Google, Software Engineer)
  7. Matteo Cimini (Assistant Professor, Univ. of Massachusetts Lowell)
  8. Spenser Bauman (Ph.D. student, Meta-tracing JIT for Racket)
  9. Di Zhong (Undergraduate Research, now Ph.D. student at Northeastern Univ.)
  10. Zeina Migeed (Research co-op from Northeastern, now Ph.D. student at UCLA)
  11. Steev Young (Undergraduate Research in Gradual Typing)
  12. Josie Bealle (Summer Research Opportunity in Computing)
  13. Andre Yuri (Summer Research Opportunity in Computing)
  14. Weiyu Miao (LinkedIn)
    Ph.D. thesis: Reflective Metaprogramming
  15. Geoffrey Belter (Apple)
    Ph.D. thesis: Efficient Generation of Sequences of Dense Linear Algebra through Auto-Tuning
  16. Shashank Bharadwaj (VMware)
  17. Jonathan Turner (Microsoft Typescript => Mozilla Rust => self employed)
  18. Erik Silkensen (Software Engineer, Meta)
  19. Neelam Agrawal (Senior Software Engineer, Google)
  20. Sri Teja Basava (Principal Software Engineer, National Instruments)
  21. Ian Karlin (Principal Engineer, HPC Ecosystems at NVIDIA)
  22. Justin Gottschlich (Parallel Computing Lab @ Intel Labs)
    Ph.D. thesis: Invalidating Transactions: Optimizations, Theory, Guarantees, and Unification
  23. Moss Prescott (SlamData)
    M.S. thesis: Speaking for the Trees: a New (Old) Approach to Languages and Syntax
  24. Christopher Schwaab (Ph.D. student at the Univ. of St. Andrews)
  25. David Broman (Full 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