We propose a new step-wise approach to proving observational equivalence, and in particular reasoning about fragility of observational equivalence. Our approach is based on what we call local reasoning. The local reasoning exploits the graphical concept of neighbourhood, and it extracts a new, formal, concept of robustness as a key sufficient condition of observational equivalence. Moreover, our proof methodology is capable of proving a generalised notion of observational equivalence. The generalised notion can be quantified over syntactically restricted contexts instead of all contexts, and also quantitatively constrained in terms of the number of reduction steps. The operational machinery we use is given by a hypergraph-rewriting abstract machine inspired by Girard's Geometry of Interaction. The behaviour of language features, including function abstraction and application, is provided by hypergraph-rewriting rules. We demonstrate our proof methodology using the call-by-value lambda-calculus equipped with (higher-order) state.

We draw new connections between deterministic, complete, and general global optimisation of continuous functions and a generalised notion of regression, using constructive type theory and computable real numbers. Using this foundation we formulate novel convergence criteria for regression, derived from the convergence properties of global optimisations. We see this as possibly having an impact on optimisation-based computational sciences, which include much of machine learning. Using computable reals, as opposed to floating-point representations, we can give strong theoretical guarantees in terms of both precision and termination. The theory is fully formalised using the safe mode of the proof assistant AGDA. Some examples implemented using an off-the-shelf constructive reals library in JAVA indicate that the approach is algorithmically promising.