Chris Jenkins

About

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.

Locations

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

Campus mailing address: 14 MacLean Hall
Office: Seamans Center for the Engineering Arts and Sciences, #1422
Email: christopher-jenkins@uiowa.edu
Website: https://cwjnkins.github.io/
Social Media: Github, Cedille Programming Language (YouTube), ResearchGate

Papers

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

Unpublished

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

Reports

Elaborating inductive definitions in Curry-style polymorphic type theory
Comprehensive exam report (2020)

paper
Bidirectional type inference in programming languages
Qualifying exam report (2018)

paper