POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Tue 16 Jan 2024 16:00 - 16:22 at Mountbatten Exhibition - Types Chair(s): Azalea Raad

A coverage type generalizes refinement types found in many functional languages with support for \emph{must}-style underapproximate reasoning. Property-based testing frameworks are one particularly useful domain where such capabilities are useful as they allow us to verify the \emph{completeness}, as well as safety, of test generators. There is a surprising connection between the kind of underapproximate reasoning coverage types offer and the style of reasoning enabled by recently proposed Incorrectness Logic frameworks. In our presentation, we propose to explore this connection more deeply, identifying mechanisms that more systematically integrate incorrectness reasoning within an expressive refinement type system and the opportunities that such integration offers to functional programmers, program verifiers, and program analyzers and related tools.

Tue 16 Jan

Displayed time zone: London change

16:00 - 17:30
TypesIncorrectness at Mountbatten Exhibition
Chair(s): Azalea Raad Imperial College London
Type-Based Incorrectness Reasoning
Zhe Zhou Purdue University, Benjamin Delaware Purdue University, Suresh Jagannathan Purdue University
Ill-Typed Programs Don't Evaluate
Steven Ramsay University of Bristol, Charlie Walpole University of Bristol