<paper_title>Look-Ahead-Freedom as Temporal Non-Interference: A Verifiable Correctness Property for Backtesting and Agentic Trading Pipelines
创建于 更新于
摘要
<paper_abstract>This work recasts look-ahead bias as temporal non-interference on a time-indexed information lattice, defines look-ahead-freedom, and develops a time-indexed pipeline calculus with a value-independent fragment for which a sound, linear-time type-and-effect system certifies look-ahead-freedom. It proves undecidability for the full language, validates a linear-time checker on pipelines within the fragment, and demonstrates empirical advantages over detectors in catching leaks while quantifying the cost of false positives. The results yield a certificate of absence of look-ahead leakage for admissible pipelines and delineate the boundary beyond which certification is impossible in general [page::1][page::5][page::18].
