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
Propositions as Types : An Introduction to Program Synthesis
ETH Zurich / Zentrum / CAB G 52, Universitätstrasse 6, Zürich, CHWelcome to Papers We Love, Zurich! We have organized a series of talks about Curry-Howard correspondence -- one of the most fruitful “coincidences” in theoretical computer science.
In the first session, Dhruv Nevatia will present “Propositions as Types” by Philip Wadler. The paper is a lucid guide to the idea that propositions can be seen as types and proofs can be seen as programs. We’ll make this concrete by working in two parallel formalisms—the simply-typed lambda calculus and intuitionistic propositional logic—and watching the same structure show up on both sides!
Once the correspondence is in place, the natural next question is: how do we actually find proofs/programs? This is the type inhabitation problem: given a type (proposition), synthesize a program (proof) of that type (proof) i.e., it inhabits it; or determine that none exists. Seen this way, inhabitation is a form of program synthesis, and it is tightly connected to proof search.
We’ll look at proof search through a saturation-style lens: rather than guessing full proofs top-down, we incrementally generate and accumulate consequences and obligations, reusing derived facts, until the target proposition is proven, or its failure has been established.Why care?
- For AI enthusiasts: it builds intuition for how “write me a correct program that does ...” can become a well-posed search problem. Turn the natural language spec into a type, then let proof search do the honest work of synthesizing a program that actually type-checks.
- For programmers and language users: Curry–Howard explains why types feel like lightweight specifications, and why “writing a term of this type” is often the same as “solving a small logical problem.”
- For logic enthusiasts: it offers a clean bridge between lambda calculi, natural deduction/sequent reasoning, and proof search/type inhabitation—setting intuition for proof assistants, typed functional programming, and program synthesis.
The talk will be 45–60 minutes, followed by discussion, Q&A and snacks. No prior background in type theory is required; basic familiarity with functions and logical implication will help.
14 attendees
Past events
2
