Typed Program Analysis Without Encodings

This conference talk from PEPM 2025 explores how programs can be viewed as both executable functions and analyzable data structures without requiring encoding. Presented by Barry Jay, the 32-minute talk challenges traditional approaches where lambda-terms must be encoded as syntax trees for analysis. Learn how tree calculus enables direct program analysis, including the groundbreaking self-application of a breadth-first self-interpreter with type [bf :∀X. ∀Y. (X→Y) → (X→Y)]. Discover a novel approach that eliminates the need for encoding typed programs into distinctive types for analysis. The presentation includes references to the published article, supplementary artifacts, and was delivered at the PEPM 2025 conference sponsored by ACM SIGPLAN, ACM SIGACT, and ACM SIGLOG.