Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Explore a 14-minute conference presentation that introduces an innovative system for incremental bidirectional typing in live programming environments using order maintenance data structures. Learn how this research addresses the implementation challenges of providing continuous semantic services like type checking and evaluation in real-time as developers edit large programs. Discover the type-theoretic specification of a small-step dynamics system that efficiently propagates type updates through marked and annotated programs, utilizing bidirectional type systems and pointer maintenance to connect bound variables to their binding locations. Examine the order maintenance data structures employed to efficiently maintain these pointers and prioritize update propagation order. Understand the formal verification of this system's equivalence to naive reanalysis through Agda theorem prover proofs, along with other crucial metatheoretic properties. Review the efficient OCaml implementation details, including impactful optimizations that achieve multiple orders of magnitude speed-up compared to from-scratch reanalysis. Analyze the performance evaluation results from large-scale stress testing that demonstrate the system's practical effectiveness for live programming environments. Access supplementary materials including the full research article, reusable artifacts, and reproduced results that support the presented findings.
