Ed Morehouse

contact You can email me at: <my_first_name>.<my_last_name> (as they appear in the URL) @<the_email_service_of_a_large_tech_company_that_formally_admonished_its_employees_against_being_evil>

about

Between 2020 and 2023 I was a postdoc with Pawel Sobocinski in the Compositional Systems and Methods Group of the Department of Software Science at TalTech University.

Between 2016 and 2019 I was a postdoc in the Department of Mathematics and Computer Science at Wesleyan University, where I taught and studied categorical semantics of formal systems.

Between 2013 and 2016 I was a postdoc with Bob Harper in the Principles of Programming Group of the Computer Science Department at Carnegie Mellon University, where I worked on computational aspects of Homotopy Type Theory.

research interests

I am interested in what category theory, type theory and proof theory can learn from one another.
I believe that categorical semantics can be quite helpful in clarifying the algebraic principles governing the properties of formal systems, which can lead us to useful insights into program development and proof search.

publications

• Cartesian Gray-Monoidal Double Categories (arXiv preprint)
• 2-Categories from a Gray Perspective (arXiv preprint)
• Normal Lax Double Functors Preserve Companions (preprint)
• Recurrence Extraction for Functional Programs through Call-by-Push-Value (arXiv preprint) (Principles of Programming Languages, 2020)
  with G. A. Kavvos, Daniel Licata, and Norman Danner
• Varieties of Cubical Sets (arXiv preprint) (Relational and Algebraic Methods in Computer Science, 2017)
  with Ulrik Buchholtz
• Homotopical Patch Theory (preprint) (Journal of Functional Programming, 2016)
  with Carlo Angiuli, Daniel Licata, and Robert Harper
• Homotopical Patch Theory (preprint) (International Conference of Functional Programming, 2014)
  with Carlo Angiuli, Daniel Licata, and Robert Harper
• An Adjunction-Theoretic Foundation for Proof Search in Intuitionistic First-Order Categorical Logic Programming (thesis, 2013)

notes, slides, code, etc.

• slides and video from my Applied Category Theory 2023 talk on Fox-cartesian structure for Gray-monoidal double categories at the University of Maryland
• slides and video from my SyCo 10 talk on locally cubical Gray categories at the University of Edinburgh
• slides from my Types 2019 talk on double-categorical models of directed type universes in Oslo
  (longer Tallinn Applied Category Theory Seminar version)
• slides from my HoTT/UF 2018 talk on ordered cubes at the University of Oxford
• slides from my RAMiCS 2017 talk on cubical varieties at the University of Lyon
• notes from a course on basic category theory at OPLSS 2016 at the University of Oregon
• videos of the lectures from that course
• slides from a talk on cubical structures for higher-dimensional type theories at Carnegie Mellon University
• notes from a course on categorical semantics for proof theory at OPLSS 2015 at the University of Oregon
• notes from a series of lectures on Tom Leinster’s globular theory of weak ω-categories at Carnegie Mellon University
• a small HoTT development in Agda using path induction and the higher groupoid structure of types
• slides from an introductory talk on functional programming at American University
• slides from a talk on categorical semantics for proof search in logic programming at Wesleyan
• slides from a talk on adjunctions as a foundation for categorical logic programming at the Université Paris 7 - Denis Diderot

teaching

In fall 2023 I taught Bowdoin's CSCI 2210: Theory of Computation.

Between 2020 and 2023 I taught TalTech's ITI0212: Functional Programming.

Between fall 2016 and spring 2018 I taught Wesleyan's COMP 112: Introduction to Programming.

In spring 2018 I taught MATH 402: Category Theory, and in spring 2017 I taught COMP 360: Quantum Information Systems.

In the summers of 2015 and 2016 I taught introduction to category theory at the Oregon Programming Languages Summer School.

other

I have written a keyboard layout for Macintosh with the mathematical symbols that I use most often. This gets changed around and expanded pretty frequently, but you're free to use it and adapt it to your own needs. Suggestions are also welcome.