Dr.-Ing. Sebastian Ullrich

	Contact Email: Bitte warten...

Research interests

Interactive theorem proving, program verification

Courses

• Laboratory: Theorem prover lab: applications in programming languages , Sommersemester 2022
• Lecture: Programming Paradigms , Wintersemester 2021/2022
• Common Excercises: Programming Paradigms - Exercises , Wintersemester 2021/2022, Beste Übung
• Laboratory: Theorem prover lab: applications in programming languages , Sommersemester 2021
• Lecture: Programming Paradigms , Wintersemester 2020/2021
• Common Excercises: Programming Paradigms - Exercises , Wintersemester 2020/2021
• Lecture: Programming Paradigms , Wintersemester 2019/2020
• Common Excercises: Programming Paradigms - Exercises , Wintersemester 2019/2020
• Lecture: Semantics of programming languages , Sommersemester 2019
• Lecture: Programming Paradigms , Wintersemester 2018/2019
• Common Excercises: Programming Paradigms - Exercises , Wintersemester 2018/2019, Beste Übung
• Laboratory: Theorem prover lab: applications in programming languages , Sommersemester 2018
• Lecture: Programming Paradigms , Wintersemester 2017/2018
• Common Excercises: Programming Paradigms - Exercises , Wintersemester 2017/2018, Beste Übung
• Lecture: Semantics of programming languages , Sommersemester 2017
• Common Excercises: Tutorial for Semantics of programming languages , Sommersemester 2017

Publications

2022

• 'do' Unchained: Embracing Local Imperativity in a Purely Functional Language (Functional Pearl)
  Proc. ACM Program. Lang. August 2022 : S. Ullrich, L. d. Moura

2021

• The Lean 4 Theorem Prover and Programming Language
  Automated Deduction -- CADE 28 2021, pp. 625--635 : L. d. Moura, S. Ullrich

2020

• Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
  Automated Reasoning 2020, pp. 167--182 : S. Ullrich, L. d. Moura

2019

• Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming (Preprint)
  31st symposium on Implementation and Application of Functional Languages September 2019 : S. Ullrich, L. d. Moura

2017

• A Metaprogramming Framework for Formal Verification
  Proc. ACM Program. Lang. September 2017 : G. Ebner, S. Ullrich, J. Roesch, J. Avigad, L. d. Moura

2016

• Verified Construction of Static Single Assignment Form
  Archive of Formal Proofs February 2016 : S. Ullrich, D. Lohner
• Verified Construction of Static Single Assignment Form
  25th International Conference on Compiler Construction 2016, pp. 67--76 (CC 2016) : S. Buchwald, D. Lohner, S. Ullrich

Projects

• Verified Construction of Static Single Assignment Form

Advised thesis projects

finished

• Static Uniqueness Analysis for Lean, masters thesis
• An Interface for Separation Logic Proofs in Lean, masters thesis
• Localizing & Presenting Lexical References in a Theorem Prover, bachelor thesis
• Proof visualization for the Lean 4 theorem prover, bachelor thesis
• Diagram Chasing in Interactive Theorem Proving, bachelor thesis
• Formally Verified Insertion of Reference Counting Instructions, bachelor thesis

Theses worked on

• Formalization of SSA-form (finished), bachelor thesis
• Simple Verification of Rust Programs via Functional Purification (finished), masters thesis