Thomas Porter

thomasjp@umich.edu

About me: I am a CSE PhD candidate at the University of Michigan, working in the Future of Programming Lab with Cyrus Omar. I am interested in livei.e. providing continuous feedback to the user, rather than, e.g., waiting for compilation. programming environments, ergonomicSome logical systems are more or less pleasant and natural for humans to use. In my opinion, more ergonomic systems tend to be concise, interpretable, and similar in structure to informal reasoning. dependent type theoriesi.e. a formal paradigm combining computer programs and mathematics proofs, which allows computers to interpret and validate proofs. A convenient and powerful system of logic. , and in combining these to support education in the formal"Formal" in the sense of symbolic - mathematics, logic, theoretical computer science, etc. and formalizedi.e. those sciences amenable to rigorous, symbolic treatment - some subset of the natural sciences, engineering, economics, linguistics, etc. sciences.