SEMBridge: Tagless-Final Program Semantics with Weakest-Precondition and Bounded-Checking Interpretations 事件

SEMBridge: Tagless-Final Program Semantics with Weakest-Precondition and Bounded-Checking Interpretations arXiv:2606.00220v1 Announce Type: cross Abstract: Formal methods provide rigorous accounts of program behavior, but practical software engineering often works through executable libraries, tests, and incremental design. This paper presents SEMBridge, a small tagless-final framework for generating weakest-precondition and bounded-checking interpretations from the same executable object progr