Type Systems for the Masses: Deriving Soundness Proofs and Efficient Checkers
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 Times are displayed in time zone: Eastern Time (US & Canada) change
15:30 - 17:30 | |||
15:30 24mTalk | Toward tool support for interactive synthesis Onward! Papers Shaon BarmanUC Berkeley, Rastislav BodikUniversity of Washington, USA, Satish ChandraSamsung Research America, Emina TorlakUniversity of Washington, Arka BhattacharyaUC Berkeley, David CullerUC Berkeley | ||
15:54 24mTalk | Type Systems for the Masses: Deriving Soundness Proofs and Efficient Checkers Onward! Papers Sylvia GreweTU Darmstadt, Sebastian ErdwegTU Darmstadt, Germany, Pascal WittmannTU Darmstadt, Mira MeziniTU Darmstadt Link to publication | ||
16:18 24mTalk | One Parser to Rule Them All Onward! Papers Link to publication DOI Pre-print Media Attached | ||
16:42 24mTalk | Isolates, Channels and Event Streams for Composable Distributed Programming Onward! Papers | ||
17:06 24mTalk | A Bootstrapping Infrastructure to Build and Extend Pharo-like Languages Onward! Papers Guillermo PolitoInria, Stéphane DucasseINRIA, France, Noury BouraqadiMines Douai, Luc FabresseMines Douai |