Most current techniques fail to achieve the dynamic update of recursive functions. A focus on execution states appears to be essential in order to implement dynamic update in this case. It indeed alleviates restrictions on the active status of updated elements. We therefore propose a novel language construct for the introspection of execution states, which matches a delimited continuation with a pattern. With formal semantics and type system, (1) unsound update programs can be detected statically and (2) the implementation does not need any specific compilation scheme. This represents one step towards formally verifiable dynamic updates and improved applicability. Beyond the simple example presented in this article, our approach can be applied to dynamically update schedulers, interrupt handlers, reactive systems and interaction loops. Categories and Subject Descriptors D.3.2 [Programming Languages]: Language Classifications--Applicative (functional) languages; D.3.3 [Programming Lang...