Formalisation of the lambda aleph Runtime
Programming Languages
2013-07-22 v1
Abstract
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 semantics, for that language. We describe a fairly comprehensive core language, and then give a small-step operational semantics based on an abstract machine. Errors are explicit in the semantics. We also prove several simple properties: that every non-terminated machine state steps to something and that reduction is deterministic once input is fixed.
Cite
@article{arxiv.1307.5277,
title = {Formalisation of the lambda aleph Runtime},
author = {Neal Glew and Tim Sweeney and Leaf Petersen},
journal= {arXiv preprint arXiv:1307.5277},
year = {2013}
}