Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Watch a 26-minute conference presentation from POPL 2018 exploring a novel type system for verifying non-deterministic higher-order functional programs. Learn how dependent refinement types can express and verify safety, termination, non-safety, and non-termination properties in programs with ∀-∃ branching behavior. Discover how the presented type system combines universal and existential reasoning within a unified framework, allowing for verification of rich properties involving program values and branching behaviors. The speakers from the University of Tsukuba and Waseda University demonstrate the system's soundness and relative completeness, while explaining how types are closed under complement due to having both modes of non-determinism. Gain insights into advanced program verification techniques that can prove path violations of safety properties using well-foundedness termination arguments.
