Using Vampire in Soundness Proofs of Type Systems

19 pages•Published: February 23, 2016

Sylvia Grewe, Sebastian Erdweg and Mira Mezini

Abstract

Type systems for programming languages shall detect type errors in programs before runtime. To ensure that a type system meets this requirement, its soundness must be formally verified. We aim at automating soundness proofs of type systems to facilitate the development of sound type systems for domain-specific languages.
Soundness proofs for type systems typically require induction. However, many of the proofs of individual induction cases only require first-order reasoning. For the development of our workbench Veritas, we build on this observation by combining automated first-order theorem provers such as Vampire with automated proof strategies specific to type systems. In this paper, we describe how we encode type soundness proofs in first-order logic using TPTP. We show how we use Vampire to prove the soundness of type systems for the simply-typed lambda calculus and for parts of a typed SQL. We report on which parts of the proofs are handled well by Vampire, and what parts work less well with our current approach.

Keyphrases: program analysis, type systems, vampire

In: Laura Kovács and Andrei Voronkov (editors). Proceedings of the 1st and 2nd Vampire Workshops, vol 38, pages 33-51.

Links:	https://easychair.org/publications/paper/46n
	https://doi.org/10.29007/22x6

BibTeX entry

@inproceedings{Vampire2014and2015:Using_Vampire_Soundness_Proofs,
  author    = {Sylvia Grewe and Sebastian Erdweg and Mira Mezini},
  title     = {Using Vampire in Soundness Proofs of Type Systems},
  booktitle = {Proceedings of the 1st and 2nd Vampire Workshops},
  editor    = {Laura Kovács and Andrei Voronkov},
  series    = {EPiC Series in Computing},
  volume    = {38},
  publisher = {EasyChair},
  bibsource = {EasyChair, https://easychair.org},
  issn      = {2398-7340},
  url       = {/publications/paper/46n},
  doi       = {10.29007/22x6},
  pages     = {33-51},
  year      = {2016}}

Download PDF Open PDF in browser