Abstract

We define a logic Sp2 that supports a simple form of assignment within a type-theoretic context that includes constructive, classical, and mixed logical formulas as datatypes. In addition to changing the value of a variable, assignment in Sp2 updates the syntactic environment with information that tracks properties of the current and old values of the variable. The current value can be constructive, but for efficiency, the old value is classical; it is not available for actual computational use. As in our earlier logic Sp1, this mixed constructivity is explained semantically by modelling classical computations as “virtual” computations. Virtual computations do not need to be evaluated because the logic is designed so that the values of these computations are computationally irrelevant for purposes of evaluating the constructive components of expressions. Sp2 is based on ideas from Constructive Type Theory and Hoare Logic: It combines proofs-as-programs, classical and constructive objects, higher-order functions, and assignment into one logic that gives programs and verification proofs a common explanation