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. |
Year | Venue | Field |
---|---|---|
2013 | CoRR | Operational semantics,Programming language,Computer science,Aleph,Theoretical computer science,Core language,Dependent type,Semantics,Technical report,Abstract machine,Lambda |
DocType | Volume | Citations |
Journal | abs/1307.5277 | 0 |
PageRank | References | Authors |
0.34 | 1 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Neal Glew | 1 | 627 | 60.50 |
Tim Sweeney | 2 | 31 | 4.29 |
Leaf Petersen | 3 | 108 | 9.65 |