Computational Higher Type Theory I: Abstract Cubical Realizability

Carlo Angiuli, Robert Harper, Todd Wilson

Brouwer's constructivist foundations of mathematics is based on an intuitively meaningful notion of computation shared by all mathematicians. Martin-Löf's meaning explanations for…