[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
The international PL group at KIT is seeking exceptional post‑docs and PhD
candidates for the AutoInc project. The AutoInc project aims to develop
formally verified methods for automatic incremental computing
(https://urldefense.com/v3/__https://incremental.dev/__;!!IBzWLUs!QT2h_4XDqA7oa-ho4xxz8a-32L48-exr4HrcGXv0AQObEVv8EqsN8Dmd90sWgTAuCNTeGL23XberOgLvLcuT2GfsnlUQ1g$
).
Achievements in the AutoInc project so far:
* Formal semantics for incremental computing that demonstrate asymptotic
speedups for loopy programs (ECOOP'25, OOPSLA'26).
* Framework for verified incremental operators that demonstrates asymptotic
speedups for relational queries and order-of-magnitude speedups for
string-processing programs (POPL'26).
Possible topics include, but are not limited to:
* Incremental semantics for richer languages (higher-order FP, OOP)
* Synthesis of provably correct incremental operators
* Design of an IR for incremental computing and verified compilation to that IR
* Static analysis and optimizations to improve incremental run-time performance
* Strategies and optimizations for reducing the memory footprint
* Applications and integration with non-incremental software
The Karlsruhe Institute of Technology (KIT) is one of Europe’s leading
institutions in engineering and natural sciences. The Department of Informatics
is one of the largest and most research-intensive computer science departments
in the country and provides a vibrant research environment.
Candidates should have a background in language implementation or formal
semantics, familiarity with proof assistants is a plus. To apply, please
contact me by email and include a CV and a description of your research
interests and experiences. I will start processing applications on March 10
until the positions are filled.
Please feel free to forward this message to any interested candidates.
