Andrew Marmaduke
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 Postdoc working in the Computational Logic Center under Dr. J. Garrett Morris. My advisor was Dr. Aaron Stump. My primary focus is PL theory and mechanization using tools like Agda and Lean4. I also work on the formal theory and implementation of Cedille2.

Teaching

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.