I'm a graduate student.

This is my website.

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.