Sitemap
A list of all the posts and pages found on the site. For you robots out there is an XML version available for digesting as well.
Pages
Posts
Future Blog Post
Published:
This post will show up by default. To disable scheduling of future posts, edit config.yml and set future: false.
Blog Post number 4
Published:
This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.
Blog Post number 3
Published:
This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.
Blog Post number 2
Published:
This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.
Blog Post number 1
Published:
This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.
portfolio
Portfolio item number 1
Short description of portfolio item number 1
Portfolio item number 2
Short description of portfolio item number 2
publications
Verified construction of static single assignment form
Published in Proceedings of the 25th International Conference on Compiler Construction, CC 2016, Barcelona, Spain, March 12-18, 2016, 2016
A metaprogramming framework for formal verification
Published in Proc. ACM Program. Lang., 2017
Counting immutable beans: reference counting optimized for purely functional programming
Published in IFL '19: Implementation and Application of Functional Languages, Singapore, September 25-27, 2019, 2019
The Lean 4 Theorem Prover and Programming Language
Published in Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, 2021
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
Published in Log. Methods Comput. Sci., 2022
'do' unchained: embracing local imperativity in a purely functional language (functional pearl)
Published in Proc. ACM Program. Lang., 2022
Lean: Past, Present, and Future (Invited Talk)
Published in 9th International Conference on Formal Structures for Computation and Deduction, FSCD 2024, July 10-13, 2024, Tallinn, Estonia, 2024
talks
Verified Construction of Static Single Assignment Form
Published:
Conference talk on our CC paper. My first conference talk!
A Metaprogramming Framework for Formal Verification
Published:
Conference talk on our ICFP paper.
Lean 4: Reimplementing Lean in Lean
Published:
Report on my internship under Leonardo de Moura during which we devised the overall design of Lean 4.
Lean 4: A Guided Preview
Published:
Even earlier progress report on Lean 4.
Lean 4: State of the ⋃
Published:
Early progress report on Lean 4.
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
Published:
Conference talk on our IJCAR paper.
Metaprogramming in Lean 4
Published:
Introduction to Lean 4 metaprogramming given together with Leonardo de Moura.
Gotta Prove Fast: Building an Ecosystem for Effortless Native Compilation of Tactics
Published:
Progress report on our native compilation efforts.
An Introduction to the Lean 4 theorem prover and programming language
Published:
Lean 4 Tutorial given together with Leonardo de Moura.
‘do’ Unchained: Embracing Local Imperativity in a Purely Functional Language
Published:
Conference talk on our ICFP paper.
Metaprograms and Proofs: Macros in Lean 4
Published:
A summary of Lean 4’s macro system with a focus on comparison to Racket’s.
Syntax Extensibility in Lean 4
Published:
Talk given during a stay at Tobias Grosser’s group. The last talk of my PhD.
Scaling Lean to the Next Millions of Lines of Proofs
Published:
Review and preview of how we scale Lean to cope with large formalization projects.
Are We Fast Yet
Published:
A summary of how we measure the performance of Lean (on e.g. Mathlib), how it compares to Lean 3, and what we have planned to further improve it.
Profiling Tools in Lean
Published:
Presented at Jasmin Blanchette’s group. Presented again at the Prospects of Formal Mathematics program at the Hausdorff Research Institute for Mathematics, Bonn, Germany.
Lean: Past, Present, and Future
Published:
Talk focusing on how Lean got to the point it is right now and where we’re going with it.
teaching
Teaching experience 1
Undergraduate course, University 1, Department, 2014
This is a description of a teaching experience. You can use markdown like any other post.
Teaching experience 2
Workshop, University 1, Department, 2015
This is a description of a teaching experience. You can use markdown like any other post.