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

15:30 - 17:30: Onward! Papers - Session the Third at Grand Station 3-5
Chair(s): Lindsey KuperIntel Labs
onward2015-papers15:30 - 15:54
Shaon BarmanUC Berkeley, Rastislav BodikUniversity of Washington, USA, Satish ChandraSamsung Research America, Emina TorlakUniversity of Washington, Arka BhattacharyaUC Berkeley, David CullerUC Berkeley
onward2015-papers15:54 - 16:18
Sylvia GreweTU Darmstadt, Sebastian ErdwegTU Darmstadt, Germany, Pascal WittmannTU Darmstadt, Mira MeziniTU Darmstadt
Link to publication
onward2015-papers16:18 - 16:42
Ali AfroozehCentrum Wiskunde & Informatica, Anastasia IzmaylovaCentrum Wiskunde & Informatica
Link to publication DOI Pre-print Media Attached
onward2015-papers16:42 - 17:06
Aleksandar ProkopecEPFL, Martin OderskyEPFL, Switzerland
onward2015-papers17:06 - 17:30
Guillermo PolitoInria, St├ęphane DucasseINRIA, France, Noury BouraqadiMines Douai, Luc FabresseMines Douai