Typed Program Analysis Without Encodings
summary
Claims a direct, unencoded program-analysis model using unlabeled binary trees and a new triage calculus with five reduction rules, where each reduction induces a subtyping rule; recursion uses a weight/wait operator to produce fixed points that are normal-form trees. Implements a breadth-first self-evaluator (BF, 392 nodes; alternate 352-node variant exists) and types it in System F extended with tree types and targeted subtyping, and the implementation and artifacts are available.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:05Programs as dual natured
- 3:19Unlabeled trees as computation
- 8:18Triage calculus introduction
- 16:01Type system for tree calculus
- 20:19Recursion in tree calculus
- 24:40Subtyping rules for expressiveness
- 25:01Typing the size function
- 27:58BF self-evaluator BFS
- 30:27System F extension
- 31:14Conclusion and Q&A
related talks
27mTowards Type Debugging using Partial Evaluation
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
24mChoice Trees: Representing Nondeterministic, Recursive, and Impure Programs in C...
19mIll-Typed Programs Don't Evaluate
56mOn Type-Based Techniques for Program Manipulation
30mComputation-Tree Semantics: An Algorithmic Approach to Structurally Defined Relations
17mFrom Traces to Program Incorrectness: A Type-Theoretic Approach
48mA History of Subtyping