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. For a good overview of my current research vision, see my short publication at the SPLASH Doctoral Symposium 2016, for which I also received the John Vlissides Award 2016. 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
  • interactive proof assistants (e.g. Isabelle/HOL and Coq)
  • fully automatic provers (e.g. Vampire, Eprover, Z3)
  • functional programming languages (e.g. Scala (the functional part), Haskell)
  • information-flow security
  • category theory

Preprints of publications (official entries see below):

  • System Description: An Infrastructure for Combining Domain Knowledge with Automated Theorem Provers
    Sylvia Grewe, Sebastian Erdweg, André Pacak, Mira Mezini. In Principles and Practice of Declarative Programming (PPDP). 2018.
  • Using Vampire with Support for Algebraic Datatypes in Type Soundness Proofs
    Sylvia Grewe, André Pacak, Mira Mezini. Proceedings of the 4th Vampire Workshop.
    EPiC Series in Computing, volume 53, 2018.
    https://easychair.org/publications/paper/9gkr
  • Exploration of Language Specifications by Compilation to First-Order Logic (journal version)
    Sylvia Grewe, Sebastian Erdweg, André Pacak, Michael Raulf, Mira Mezini. Science of Computer Programming, PPDP Special Issue
    Elsevier, 2018.
    [Link to PDF]
  • VeriTaS: Verification of Type System Specifications – Mechanizing Domain Knowledge about Progress and Preservation Proofs
    Sylvia Grewe. Companion Proceedings of the 2016 ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for Humanity, SPLASH 2016 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. In Proceedings of the 3rd Vampire Workshop. EPiC Series in Computing, 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]

Co-authored entries in the Isabelle Archive of Formal Proofs:

Publications

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

2017

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

Automating Proof Steps of Progress Proofs: Comparing Vampire and Dafny.
[Online-Edition: http://easychair.org/publications/paper/Automating_Proof_Ste...]
In: Vampire 2016. Proceedings of the 3rd Vampire Workshop. EPiC Series in Computing, 44. , pp. 33-45.
[Book section] , (2017)

2016

Grewe, Sylvia :
VeriTaS: Verification of type system specifications: Mechanizing domain knowledge about progress and preservation proofs.
[Online-Edition: http://doi.acm.org/10.1145/2984043]
In: Companion Proceedings of the 2016 ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for Humanity, SPLASH 2016. Amsterdam, Netherlands , pp. 12-14.
[Book section] , (2016)

Grewe, Sylvia ; Erdweg, Sebastian ; Raulf, Michael ; Mezini, Mira :
Exploration of language specifications by compilation to first-order logic.
[Online-Edition: http://doi.acm.org/10.1145/2967973.2968606]
In: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, Edinburgh, United Kingdom, September 5-7, 2016. ACM , pp. 104-117.
[Book section] , (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 Nov 16 05:38:31 2018 CET.