I'm a PhD student in the UChicago CS department. I'm generally interested in logic and computing. I've spent some time thinking about proof complexity and SAT-solvers, but more recently I've been thinking about pure type systems and normalization.
I'm currently a teaching assistant for the course MPCS 50103: Math for Computer Science: Discrete Math taught by Amitabh Chaudhary. My office hours are Tuesdays 1-3PM in JCL 267 and on Zoom.
Nathan Mull. Weak Normalization implies Strong Normalization in Non-Dependent Persistent Pure Type Systems. In preparation, draft upon request.
Nathan Mull. An Irrelevance-Eliminating Translation for Tiered Pure Type Systems. Submitted to TYPES 2022 Post-Proceedings. [pdf]
Nathan Mull. Strong Normalization from Weak Normalization in Non-Dependent Pure Type Systems via Thunkification. Research Report, 2022. [pdf]
Nathan Mull. A Generalized Translation of Pure Type Systems. Extended Abstract in the Proceedings of the 28th International Conference on Types for Proofs and programs (TYPES), 2022. [abstract,slides]
Nathan Mull, Shuo Pang, and Alexander Razborov. On CDCL-based Proof Systems with the Ordered Decision Strategy. SIAM Journal of Computing, 2022. (Conference version appeared in SAT 2020) [pdf]
Nathan Mull, Daniel J. Fremont, and Sanjit A. Seshia. On the Hardness of SAT with Community Structure. In the Proceedings of the 19th International Conference on the Theory and Application of Satisfiability Solving (SAT), 2016. [pdf]
(10/19/22) I gave an informal talk on Girard's paradox for the UChicago Theory Lunch. I primarily wanted to emphasize why Martin-Löf might have include the axiom 'Type is a Type' in his type theory despite being fully aware of classical set-theoretic paradoxes. [slides]
I've had the pleasure of teaching CMSC 10500: Fundamentals of Computer Programming in Swift for several years now. In the last few goes, I was able to compile my notes into a GitBook. The material is loosely based on that of SICP and Composing Programs, two invaluable introductory programming resources. [link]
There are several proofs of false written in Idris floating around on the internet. This one is an implementation of Girard's paradox which takes advantage of what seems to be a bug in the way universe levels are determined. [link]
I'm pretty sure it's impossible to find a copy of Turing's original proof that STLC is weakly normalizing (as published by R.O. Gandy), so I decided to type up a version myself to make available here. [pdf]
Every once in a while, I write a bit of poetry. [link]
Check my CV for contact information.