| Autor: |
Glew, Neal, Sweeney, Tim, Petersen, Leaf |
| Rok vydání: |
2013 |
| Předmět: |
|
| Druh dokumentu: |
Working Paper |
| Popis: |
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. |
| Databáze: |
arXiv |
| Externí odkaz: |
|
