Rewriting for Sound and Complete Union, Intersection and Negation Types
Implementing the type system of a programming language is a critical task that is often done in an ad-hoc fashion. Whilst this makes it hard to ensure the system is sound, it also makes it difficult to extend as the language evolves. We are interested in describing type systems using declarative rewrite rules from which an implementation can be automatically generated. Whilst not all type systems are easily expressed in this manner, those involving unions, intersections and negations are well-suited for this.
In this paper, we consider a relatively complex type system involving unions, intersections and negations developed previously. This system was not developed with rewriting in mind, though clear parallels are immediately apparent from the original presentation. For example, the system presented required types be first converted into a variation on Disjunctive Normal Form. We identify that the original system can, for the most part, be reworked to enable a natural expression using declarative rewrite rules. We present an implementation of our rewrite rules in the Whiley Rewrite Language (WyRL), and report performance results compared with a hand-coded solution.
this URL might only work when visiting from a http://www.sigplan.org/ URL.
David (@whileydave) graduated with a PhD from Imperial College London in 2005, and took up a lecturer position at Victoria University of Wellington, NZ. David’s PhD thesis was on efficient algorithms for pointer analysis of C, and his techniques have since been incorporated into GCC. His interests are in programming languages, compilers and static analysis.
Since 2009, he has been developing the Whiley Programming Language (whiley.org) which is designed specifically to simplify program verification. Prior to that, David developed the Java Compiler Kit (JKit), which is an open source Java Compiler aimed at simplifying static analysis.
David has previously interned at Bell Labs, New Jersey, where he worked on compilers for FPGAs; and also at IBM Hursely, UK, where he worked with the AspectJ development team on profiling systems.
Mon 23 OctDisplayed time zone: Tijuana, Baja California change
15:30 - 17:00 | |||
15:30 25mTalk | Type Qualifiers as Composable Language Extensions GPCE 2017 DOI Authorizer link | ||
15:55 25mTalk | Accurate Reification of Complete Supertype Information for Dynamic Analysis on the JVM GPCE 2017 Andrea Rosà University of Lugano, Switzerland, Eduardo Rosales University of Lugano, Switzerland, Walter Binder University of Lugano, Switzerland DOI Authorizer link | ||
16:20 25mTalk | Rewriting for Sound and Complete Union, Intersection and Negation Types GPCE 2017 David J. Pearce Victoria University of Wellington, New Zealand DOI Authorizer link |