Onward! 2015
Sun 25 - Fri 30 October 2015 Pittsburgh, Pennsylvania, United States
co-located with SPLASH 2015
Thu 29 Oct 2015 15:54 - 16:18 at Grand Station 3-5 - Session the Third Chair(s): Lindsey Kuper

The correct definition and implementation of non-trivial type systems is difficult and requires expert knowledge, which is not available to developers of domain-specific languages and specialized APIs in practice. We propose Veritas, a workbench that simplifies the development of sound type systems. Veritas provides a single, high-level specification language for type systems, from which it automatically tries to derive soundness proofs and efficient and correct type-checking algorithms. For verification, Veritas combines off-the-shelve automated first-order theorem provers with automated proof strategies specific to type systems. For deriving efficient type checkers, Veritas provides a collection of optimization strategies whose applicability to a given type system is checked through verification on a case-by-case basis. We have developed a prototypical implementation of Veritas and used it to verify type soundness of the simply-typed lambda calculus and of parts of typed SQL. Our experience suggests that a high degree of automation is possible for type systems of domain-specific languages.

Thu 29 Oct

Displayed time zone: Eastern Time (US & Canada) change

15:30 - 17:30
Session the ThirdOnward! Papers at Grand Station 3-5
Chair(s): Lindsey Kuper Intel Labs
15:30
24m
Talk
Toward tool support for interactive synthesis
Onward! Papers
Shaon Barman UC Berkeley, Rastislav Bodík University of Washington, USA, Satish Chandra Samsung Research America, Emina Torlak University of Washington, Arka Bhattacharya UC Berkeley, David Culler UC Berkeley
15:54
24m
Talk
Type Systems for the Masses: Deriving Soundness Proofs and Efficient Checkers
Onward! Papers
Sylvia Grewe TU Darmstadt, Sebastian Erdweg TU Darmstadt, Germany, Pascal Wittmann TU Darmstadt, Mira Mezini TU Darmstadt
Link to publication
16:18
24m
Talk
One Parser to Rule Them All
Onward! Papers
Ali Afroozeh Centrum Wiskunde & Informatica, Anastasia Izmaylova Centrum Wiskunde & Informatica
Link to publication DOI Pre-print Media Attached
16:42
24m
Talk
Isolates, Channels and Event Streams for Composable Distributed Programming
Onward! Papers
Aleksandar Prokopec EPFL, Martin Odersky EPFL, Switzerland
17:06
24m
Talk
A Bootstrapping Infrastructure to Build and Extend Pharo-like Languages
Onward! Papers
Guillermo Polito Inria, Stéphane Ducasse INRIA, France, Noury Bouraqadi Mines Douai, Luc Fabresse Mines Douai