About us
Love talking about papers? So do we!
Do you have a paper within the realm of computing that excites you — recent or classic — and want to share it with others? Or would you enjoy hearing accessible, enthusiastic explanations of important research?
Whether you have implemented the ideas, used them in a project, or simply want to learn and discuss, this is a welcoming, inclusive space for presenters and listeners alike: we celebrate diverse perspectives, encourage practical demos and honest struggles. Everyone — students, researchers, engineers and curious minds — is invited.
Logistics — we meet monthly in Zürich, usually on a Thursday, 18:15–20:00; RSVP on Meetup.
Subjects — papers live within the broad realms of computing and computer science, kept intentionally open-ended.
Audience — ideal for anyone who wants accessible explanations of complex computer-science papers, where the maths is typically simplified.
Culture — inclusive, respectful and welcoming to diverse perspectives.
Presentation format — talks are typically 45–60 minutes, followed by discussion, Q&A and networking.
We are curating this repository for papers presented at PWL Zürich. You can contribute by adding Pull Requests for papers, code, and/or links to our repository here. We keep a list of papers that we would like to talk about. Slides of all our previous talks will be made available (if available) on our website.
We follow the Papers We Love Code of Conduct.
More details can be found on the event page.
Upcoming events
1
Techniques for Program Verification
ETH Zurich, CAB G 56, Universitätstrasse 6, 8006, Zurich, CHWe are back!
In this session, George Zakhour, a PhD student at the Programming Group at the University of St.Gallen will present "Techniques for Program Verification", focusing particularly on e-graphs.
E-graphs are at the heart of SMT solvers, a cornerstone of automated reasoning that powers applications from program verification to automated theorem proving. They are used for efficiently maintaining equalities and equivalence relations. Originally introduced in Greg Nelson's seminal 1980 PhD thesis, they gained widespread popularity for compiler optimization, program synthesis, and software testing thanks to the egg library (POPL' 21). In this talk, we will revisit Nelson's thesis, implement an e-graph live from scratch, and put it to work.
Why care?
- For verification enthusiasts: the e-graph is the congruence closure that propagates equalities from one theory to all the others. They allow you to build a large theory compositionally from smaller ones.
- For type system enthusiasts: e-graphs are the solvers of type inference constraints.
- For compiler enthusiasts: e-graphs eliminate phase ordering by searching many equivalent program optimizations at once.
The talk will be 45–60 minutes, followed by discussion, Q&A and snacks. No prior background in SMTs is required; basic familiarity with compilers and formal methods will help.
8 attendees
Past events
3
