Blogs (9) >>
SPLASH 2016
Sun 30 October - Fri 4 November 2016 Amsterdam, Netherlands
Tue 1 Nov 2016 10:30 - 11:10 at Geneva - Session 2

Developing a type system with a soundness proof is hard. The VeriTaS project aims at simplifying the development of sound type systems through automation of soundness proofs and through automated derivation of efficient type checkers from sound type system specifications. Within the VeriTaS project, I focus on developing an interface for the verification of progress and preservation proofs which shall automate standard parts such proofs. To achieve this, I propose to identify recurring proof strategies in progress and preservation proofs from the literature, to develop a format for abstractly representing these proof strategies, and to mechanize them by integrating with existing theorem provers.

Tue 1 Nov

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10
10:30
40m
Talk
VeriTaS: Verification of Type System Specifications
Doctoral Symposium
Sylvia Grewe TU Darmstadt
Pre-print
11:10
40m
Talk
Language Support for Verifiable SDNs
Doctoral Symposium