constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
Separation logic is an extension of Hoare logic used to reason about memory separation and memory sharing in programs with pointer structures.
Last revised on January 18, 2023 at 10:02:01. See the history of this page for a list of all contributions to it.