The pattern-match safety problem is to verify that a given functional program will never crash due to non-exhaustive patterns in its function definitions. We present a refinement type system that can be used to solve this problem. The system extends ML-style type systems with algebraic datatypes by a limited form of structural subtyping and environment-level intersection. We describe a fully automatic, sound and complete type inference procedure for this system which, under reasonable assumptions, is worst-case linear-time in the program size. Compositionality is essential to obtaining this complexity guarantee. A prototype implementation for Haskell is able to analyse a selection of packages from the Hackage database in a few hundred milliseconds.
Fri 17 JunDisplayed time zone: Pacific Time (US & Canada) change
13:30 - 14:50 | |||
13:30 20mTalk | (POPL 2022) Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs SIGPLAN Track Charles Yuan Massachusetts Institute of Technology, Christopher McNally Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology Link to publication DOI Authorizer link Pre-print | ||
13:50 20mTalk | (ICFP 2020) Compiling effect handlers in capability-passing style SIGPLAN Track Philipp Schuster University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen, Klaus Ostermann University of Tuebingen Link to publication DOI Authorizer link Pre-print | ||
14:10 20mTalk | (POPL 2021) Intensional Datatype Refinement SIGPLAN Track | ||
14:30 20mTalk | (POPL 2021) A Verified Optimizer for Quantum Circuits SIGPLAN Track Kesha Hietala University of Maryland, Robert Rand University of Chicago, Shih-Han Hung University of Maryland, USA, Xiaodi Wu Department of Computer Science, Institute for Advanced Computer Studies, and Joint Center for Quantum Information and Computer Science, University of Maryland, MD, Michael Hicks University of Maryland at College Park |