Formalisation of the lambda aleph Runtime

TL;DR

This paper formalizes the runtime semantics of a multivalued dependent type language, providing an operational semantics with explicit errors and proving key properties like progress and determinism.

Contribution

It introduces a formal operational semantics for a novel dependent typing language based on multivalued terms, with proofs of fundamental properties.

Findings

Every non-terminated state advances to another state

Reduction process is deterministic given fixed input

Explicit error handling in the semantics

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.