Ed Morehouse

contact mailing address TalTech Department of Software Science Akadeemia tee 21B 12618 Tallinn Estonia email edward.morehouse@taltech.ee

about

I am 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 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

Since the spring of 2020 I have co-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.

As a graduate student I taught introduction to calculus and served as teaching assistant for linear algebra, discrete math, mathematical logic, automata theory, programming languages and several introductory programming courses.

other

I enjoy being outside. In most years of graduate school I helped organize a fall-break trip for graduate and visiting international students. Most recently, we went hiking in Acadia National Park.

In 2008 I was elected to the educational policy committee of my university. Now I have a much deeper appreciation for the mundane but difficult work that goes into making possible all the visible aspects of the functioning of the institution. It felt a bit like when I took a summer job at Universal Studios as an undergraduate.

I have been an unenthusiastic user of LaTeX for a few years now. Lately I have become a somewhat more enthusiasic user of XeTeX and Will Robertson's excellent fontspec and unicode-math packages, which save me loads of typing and clutter. 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.