Chris Jenkins



4th year CS PhD student working with the Computational Logic Center at the University of Iowa, advised by Dr. Aaron Stump. Research assistantship working on Cedille, an experimental dependent type theory.

Research interest is programming language theory, specifically (dependent) type theory, inductive definitions, recursion schemes, elaboration, and bidirectional type inference. Also interested in programming language semantics, including categorical and realizability. CV.


Mathematical Sciences University of Iowa, Iowa City, IA 52236.


  • Strong Functional Pearl: Harper's Regular-Expression Matcher in Cedille

    Stump, Aaron and Jenkins, Christopher and Spahn, Stephan and McDonald, Colin. ICFP 2020

    paper bib talk

  • Efficient lambda encodings for Mendler-style coinductive types in Cedille

    Jenkins, Christopher and Stump, Aaron and Diehl, Larry. MSFP 2020

    paper bib slides talk code

  • Quotients by Idempotent Functions in Cedille

    Marmaduke, Andrew and Jenkins, Christopher and Stump, Aaron. TFP 2019

    paper bib code

  • Monotone Recursive Types and Recursive Data Representations in Cedille

    Jenkins, Christopher and Stump, Aaron. Submitted to J. MSCS (2019)

    paper bib code

  • Spine-local Type Inference

    Jenkins, Christopher and Stump, Aaron. IFL 2018

    paper bib slides appendix


  • Elaborating course-of-values induction in Cedille

    Jenkins, Christopher and Firsov, Denis and Diehl, Larry and McDonald, Colin and Stump, Aaron. (2020)

    paper appendix code


  • Elaborating inductive definitions in Curry-style polymorphic type theory

    Comprehensive exam report (2020)


  • Bidirectional type inference in programming languages

    Qualifying exam report (2018)