[ajbt200128]

Of note, CMU produces a bunch of functional programming research, including a whole homotopy type theory department, so this is a quality source.