SPLASH 2016 (series) / Scala 2016 (series) / Scala /
A Generic Algorithm for Checking Exhaustivity of Pattern Matching (Short Paper)
Sun 30 Oct 2016 11:20 - 11:45 at Matterhorn 2 - Types
Algebraic data types and pattern matching are key features of functional programming languages. Exhaustivity checking of pattern matching is a safety belt that defends against unmatched exceptions at runtime and boosts type safety. However, the presence of language features like inheritance, typecase, traits, GADTs, path-dependent types and union types makes the checking difficult and the algorithm complex.
In this paper we propose a generic algorithm that decouples the checking algorithm from specific type theories. The decoupling makes the algorithm simple and enables easy customization for specific type systems.
I’m a PhD student at EPFL. My interested areas are type systems, effect systems, programming languages, and various logics.
Sun 30 Oct Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Sun 30 Oct
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:10 | |||
10:30 25mTalk | Implementing Higher-Kinded Types in Dotty Scala Martin OderskyEPFL, Switzerland, Guillaume MartresEPFL, Switzerland, Dmitry PetrashkoEPFL, Switzerland DOI Pre-print Media Attached | ||
10:55 25mTalk | Semantics-Driven Interoperability between Scala.js and JavaScript Scala Sébastien DoeraeneEPFL, Switzerland, Tobias SchlatterEPFL, Switzerland, Nicolas StuckiEPFL, Switzerland DOI Pre-print | ||
11:20 25mTalk | A Generic Algorithm for Checking Exhaustivity of Pattern Matching (Short Paper) Scala Fengyun LiuEPFL, Switzerland DOI Media Attached | ||
11:45 25mTalk | Scaps: Type-Directed API Search for Scala Scala Lukas Wegmann1plusX, Switzerland, Farhad MehtaUniversity of Applied Sciences Rapperswil, Switzerland, Peter SommerladUniversity of Applied Sciences Rapperswil, Switzerland, Mirko StockerUniversity of Applied Sciences Rapperswil, Switzerland DOI File Attached |