Formalisation of the lambda aleph Runtime

Neal Glew, Tim Sweeney, Leaf Petersen

In previous work we describe a novel approach to dependent typing based on a multivalued term language. In this technical report we formalise the runtime, a kind of operational sem…