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

splash-2016-ds
10:30 - 12:10: Doctoral Symposium - Session 2 at Geneva
splash-2016-ds147799260000010:30 - 11:10
Talk
Pre-print
splash-2016-ds147799500000011:10 - 11:50
Talk