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.
- Simulating large eliminations in Cedille (extended abstract)
Jenkins, Christopher and Marmaduke, Andrew and Stump, Aaron. TYPES 2021
- Zero-cost Constructor Subtyping
Marmaduke, Andrew and Jenkins, Christopher and Stump, Aaron. IFL 2020
- Strong Functional Pearl: Harper's Regular-Expression Matcher in Cedille
Stump, Aaron and Jenkins, Christopher and Spahn, Stephan and McDonald, Colin. ICFP 2020
- Efficient lambda encodings for Mendler-style coinductive types in Cedille
Jenkins, Christopher and Stump, Aaron and Diehl, Larry. MSFP 2020
- Quotients by Idempotent Functions in Cedille
Marmaduke, Andrew and Jenkins, Christopher and Stump, Aaron. TFP 2019
- Monotone Recursive Types and Recursive Data Representations in Cedille
Jenkins, Christopher and Stump, Aaron. Submitted to J. MSCS (2019)
- Spine-local Type Inference
Jenkins, Christopher and Stump, Aaron. IFL 2018