Manuscript En03-A@1 · En03-A.tex · remark · 5398614e

Remark: Output typing

Restricted destructive deferred readout › Geometry and continuation · lines 1175–1181

En03-A@1#rem:output-typing

The immediate output has type $Bit^{\otimes n} \otimes B_{T}$ . The deferred output additionally contains $S$ . It must be returned or consumed by a well-typed continuation. Inaccessibility does not create a weakening rule.

Nearby in this section

theorem: Theorem: Restricted destructive deferred readout
remark: Remark: Input-dependent selection
example: Example: Access to excluded registers
section: Geometry and continuation