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 (opens in new tab) , 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 (opens in new tab) ] - 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 (opens in new tab) ] - 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 (opens in new tab) ] - 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 (opens in new tab) ] - 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 (opens in new tab) ] - 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 (opens in new tab) ]
Co-authored entries in the Isabelle Archive of Formal Proofs:
- An Isabelle/HOL Formalization of the Modular Assembly Kit for Security Properties
https://www.isa-afp.org/entries/Modular_Assembly_Kit_Security.html - A Formalization of Strong Security:
http://afp.sourceforge.net/entries/Strong_Security.shtml - A Formalization of Declassification with WHAT-and-WHERE Security:
http://afp.sourceforge.net/entries/WHATandWHERE_Security.shtml - A Formalization of Assumptions and Guarantees for Compositional Noninterference:
http://afp.sourceforge.net/entries/SIFUM_Type_Systems.shtml
Publications
Error on loading data
An error has occured when loading publications data from TUbiblio. Please try again later.
-
{{ year }}
-
; {{ creator.name.family }}, {{ creator.name.given }}{{ publication.title }}.
; {{ editor.name.family }}, {{ editor.name.given }} (eds.); ; {{ creator }} (Corporate Creator) ({{ publication.date.toString().substring(0,4) }}):
In: {{ publication.series }}, {{ publication.volume }}, In: {{ publication.book_title }}, In: {{ publication.publication }}, {{ publication.journal_volume}} ({{ publication.number }}), ppp. {{ publication.pagerange }}, {{ publication.place_of_pub }}, {{ publication.publisher }}, {{ publication.institution }}, {{ publication.event_title }}, {{ publication.event_location }}, {{ publication.event_dates }}, ISSN {{ publication.issn }}, e-ISSN {{ publication.eissn }}, ISBN {{ publication.isbn }}, DOI: {{ publication.doi.toString().replace('http://','').replace('https://','').replace('dx.doi.org/','').replace('doi.org/','').replace('doi.org','').replace("DOI: ", "").replace("doi:", "") }}, Official URL, {{ labels[publication.type]?labels[publication.type]:publication.type }}, {{ labels[publication.pub_sequence] }}, {{ labels[publication.doc_status] }} - […]
-
Number of items in this list: >{{ publicationsList.length }}
Only the {{publicationsList.length}} latest publications are displayed here.