Andrew Marmaduke
andrew-marmaduke [at] uiowa [dot] edu
Mathematical Sciences, University of Iowa, Iowa City, IA 52241
Mailing Address: 14 MacLean Hall
Office: Seamans Center for the Engineering Arts and Sciences, #1422

About

I'm a Computer Science PhD student working in the Computational Logic Center. My advisor is Dr. Aaron Stump. I work with Aaron and others on Cedille. I am interested in programming language theory, logic, and the formalization of mathematics.
My current research revolves around how Cedille's unique feature set (dependent intersections, equality of well-scoped untyped terms, and erased function spaces) can be used to capture and construct many of the ideas in other languages (such as large eliminations, induction-induction, induction-recursion, etc).

Google Scholar, DBLP, CV

Teaching

Algorithms

Conference and Symposium Proceedings

  1. Best Student Paper Award. Impredicative Encodings of Inductive-Inductive Data in Cedille. Andrew Marmaduke, Larry Diehl, Aaron Stump. Trends in Functional Programming (TFP 2023) doi
  2. Simulating Large Eliminations in Cedille. Christa Jenkins, Andrew Marmaduke, Aaron Stump. 27th International Conference on Types for Proofs and Programs (TYPES 2021) doi
  3. Zero-Cost Constructor Subtyping. Andrew Marmaduke, Christa Jenkins, Aaron Stump. Implementation and Application of Functional Languages (IFL 2020) doi
  4. Quotients by Idempotent Functions in Cedille. Andrew Marmaduke, Christa Jenkins, Aaron Stump. Trends in Functional Programming (TFP 2019) doi

Talks

  1. Carving out a proof theory from Cedille's Core. Midwest Programming Language Summit (MWPLS) 2023 pdf

Unpublished Works

  1. A Simple Coarse-Grained Model of a Carbon Nanotube Forest Interacting with a Rigid Substrate. Andrew Marmaduke. Master Thesis. The University of Akron (2015)

Tools

  1. olette. An optimal lambda evaluation toy for graphically exploring reductions one at a time without an oracle to decide matching of fans. Implemented with the help of Macy Schmidt.