|
|
|
Contact Phone: +49 721 608-47401 Email:
Bitte warten... |
IPD Prof. Snelting Room 022, Building 50.34 Am Fasanengarten 5 76131 Karlsruhe Germany |
|
Consultation Hours: wann immer ich da bin / whenever I'm in my office |
|
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
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