index

Sylvia Grewe, M.Sc

I am a doctoral researcher in the Software Technology Group. I currently work on automating soundness proofs for type systems of domain specific languages. Before joining the Software Technology Group in August 2014, I worked on formalizing different concepts from the area of information-flow security within the proof assistant Isabelle/HOL (see entries in the Isabelle Archive of Formal Proofs below).

I obtained my Bachelor's degree in computer science at TU Darmstadt in 2010. From 2010 to 2012, I studied in a double degree program between TU Darmstadt and EURECOM in Sophia Antipolis (southern France). During this time, I studied 3 semesters in Sophia Antipolis and spent one semester writing my master's thesis in TU Darmstadt in the MAIS group. In September 2012, I obtained both the degrees Master of Science in computer science from TU Darmstadt and Diplôme d'ingénieur from TELECOM ParisTech in the name of EURECOM.

My research interests include:

  • type systems and type theory
  • formal verification of type systems
  • proof assistants (Isabelle/HOL and Coq) and fully automatic provers
  • functional programming languages
  • information-flow security
  • category theory

Preprints of publications (official entries see below):

  • VeriTaS: Verification of Type System Specifications – Mechanizing Domain Knowledge about Progress and Preservation Proofs
    Sylvia Grewe. To appear in SPLASH Doctoral Symposium. ACM, 2016.
    [Link to PDF]
  • Exploration of Language Specifications by Compilation to First-Order Logic
    Sylvia Grewe, Sebastian Erdweg, Michael Raulf, and Mira Mezini. In Principles and Practice of Declarative Programming (PPDP). ACM, 2016.
    [Link to PDF]
  • Automating Proof Steps of Progress Proofs: Comparing Vampire and Dafny
    Sylvia Grewe, Sebastian Erdweg, and Mira Mezini. To appear in 3rd Vampire Workshop EPiC, 2016.
    [Link to PDF]
  • Type Systems for the Masses: Deriving Soundness Proofs and Efficient Checkers
    Sylvia Grewe, Sebastian Erdweg, Pascal Wittmann, and Mira Mezini. In Proceedings of Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software (Onward). ACM, 2015.
    [Link to PDF]
  • Using Vampire in Soundness Proofs of Type Systems
    Sylvia Grewe, Sebastian Erdweg, and Mira Mezini. In Proceedings of Vampire Workshop. EPiC, 2015.
    [Link to PDF]

Entries in the Isabelle Archive of Formal Proofs:

Publications

Group by: Date | Item type | No grouping
Jump to: 2016 | 2015
Number of items: 2.

2016

Grewe, Sylvia ; Erdweg, Sebastian ; Mezini, Mira
Kovács, Laura ; Voronkov, Andrei (eds.) :

Using Vampire in Soundness Proofs of Type Systems.
[Online-Edition: http://easychair.org/publications/paper/Using_Vampire_in_Sou...]
In: EPiC Series in Computing .
[Conference or workshop item], (2016)

2015

Grewe, Sylvia ; Erdweg, Sebastian ; Wittmann, Pascal ; Mezini, Mira :
Type Systems for the Masses: Deriving Soundness Proofs and Efficient Checkers.
[Online-Edition: http://doi.acm.org/10.1145/2814228.2814239]
In: 2015 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Onward! 2015, Pittsburgh, PA, USA, October 25-30, 2015. ACM , pp. 137-150.
[Book section], (2015)

This list was generated on Fri Sep 23 07:50:53 2016 CEST.