Symbolic Types for Lenient Symbolic Execution

Watch a 25-minute conference presentation from POPL 2018 exploring lambda_sym, a typed λ-calculus designed for lenient symbolic execution. Discover how researchers from Northeastern University and University of Washington developed a type system that ensures safe handling of symbolic values while accommodating language constructs that don't recognize them. Learn about the integration of symbolic types and mutable state with occurrence typing, along with the introduction of concreteness polymorphism to maintain soundness. See how these theoretical foundations were implemented in Typed Rosette, a typed extension of the solver-aided Rosette language, with demonstrations of its practical application across a substantial codebase. Gain insights into solver-aided languages, symbolic execution, type systems, and macro development through this academic exploration of safer symbolic execution techniques.