Georg Neis
Affiliation: MPI-SWS & Saarland University
Email: neis@mpi-sws.org
Phone: (+49) 681 9303 8714
Office: Room 334, Campus E1 5, 66123 Saarbrücken
I'm a student at the Foundations of Programming group here
at MPI-SWS. My advisor is Derek Dreyer. In 2010, I did an internship at Microsoft Research in Cambridge, working with Nick Benton. In 2012, I received a Google European Doctoral Fellowship in Programming Technology. In 2014, I did an internship at Google Munich, working in the V8 team.
To be continued...
Research
Pilsner: A Compositionally Verified Compiler for a Higher-Order Imperative LanguageGeorg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, and Viktor Vafeiadis.
In 2015 ACM SIGPLAN International Conference on Functional Programming (ICFP 2015).
Details: (abstract, paper, technical appendix, coq code)
A Logical Step Forward in Parametric Bisimulations
Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis.
Technical Report MPI-SWS-2014-003, January 2014.
Details: (abstract, paper with technical appendix, coq code)
The Power of Parameterization in Coinductive Proof
Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis.
In 2013 ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013).
Details: (abstract, paper, coq code)
The Impact of Higher-Order State and Control Effects on Local Relational Reasoning
Derek Dreyer, Georg Neis, and Lars Birkedal.
In Journal of Functional Programming (JFP), 22(4&5):477--528, September 2012.
Special issue devoted to selected papers from ICFP 2010.
This is a significantly revised and expanded version of our ICFP 2010 paper.
Details: (abstract, paper, errata)
Paco: A Coq Library for Parameterized Coinduction
Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis.
Announced on the coq-club mailing list, August 2012.
Details: (description, download, tutorial)
The Transitive Composability of Relation Transition Systems
Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis.
Technical Report MPI-SWS-2012-002, May 2012.
Details: (abstract, paper, coq code)
The Marriage of Bisimulations and Kripke Logical Relations
Chung-Kil Hur, Derek Dreyer, Georg Neis, and Viktor Vafeiadis.
In 2012 ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012).
Details: (abstract, paper, appendix, coq code)
Self-Adjusting Stack Machines
Matthew Hammer, Georg Neis, Umut Acar, and Yan Chen.
In 2011 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2011).
Details: (abstract, paper, technical report)
Non-Parametric Parametricity
Georg Neis, Derek Dreyer, and Andreas Rossberg.
In Journal of Functional Programming (JFP), 21(4&5):497--562, September 2011.
Special issue devoted to selected papers from ICFP 2009.
This is a revised and expanded version of our ICFP 2009 paper.
Details: (abstract, paper)
The Impact of Higher-Order State and Control Effects on Local Relational Reasoning
Derek Dreyer, Georg Neis, and Lars Birkedal.
In 2010 ACM SIGPLAN International Conference on Functional Programming (ICFP 2010).
Nominated by ACM SIGPLAN for a CACM Research Highlight!
Details: (abstract, paper, appendix, errata)
This paper is superseded by the JFP version cited above.
A Relational Modal Logic for Higher-Order Stateful ADTs
Derek Dreyer, Georg Neis, Andreas Rossberg, and Lars Birkedal.
In 2010 ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010).
Details: (abstract, paper, appendix)
Non-Parametric Parametricity
Georg Neis, Derek Dreyer, and Andreas Rossberg.
In 2009 ACM SIGPLAN International Conference on Functional Programming (ICFP 2009).
Details: (abstract, paper, long version (my master's thesis))