Philip Wadler
where else to find them
what they talk about
all 9 in the filters
where they keep going back
- Strange Loop2 editions2015–2018
- Lambda Days2 editions2016–2018
all 9 in the filters
on a stage with
all 13 in the filters
who talks about the same things
- Bartosz Milewski10 talks
- Ranjit Jhala19 talks
- Simon Peyton Jones26 talks
- Alejandro Serrano9 talks
- Steve Zdancewic19 talks
- Alexander Konovalov8 talks
| title | conference | date |
|---|---|---|
| From Lambda to Ledger: An Architectural Comparison of Plinth and Plutarch | FUNARCH 2026 | 2026-08-29 |
Compares two Cardano smart‑contract approaches: a GHC plugin (Plinth) vs an embedded DSL (Plutarch), implements seven validators and measures source size… | ||
| Plinth: A Plugin-Powered Language Built on Haskell (Experience Report) | Haskell 2025 | 2025-10-16 |
Plinth is a production DSL that reuses a subset of Haskell syntax, compiles via a GHC plugin into PIR → typed Plutus Core (System Fω with iso-recursive types)… | ||
| Haskell equations, thirty-eight years later | Haskell 2025 | 2025-10-16 |
Proposal introduces a compact syntax that makes equation groups unordered unless annotated with a trailing otherwise keyword, so order only matters when… | ||
| Featherweight Go | OOPSLA 2020 | 2020-11-15 |
Defines a minimal core language Featherweight Go (FG) and its generic extension Featherweight Generic Go (FGG), proves a semantics-by-translation claim that… | ||
| (Programming Languages) in Agda = Programming (Languages in Agda) | Full Stack Fest 2019 | 2019-09-04 |
An executable Agda textbook implements language definitions and checks proofs as programs so examples like addition and a 20‑line proof that plus is… | ||
| Categories for the Working Hacker | Strange Loop 2018 | 2018-09-26 |
Shows concrete equivalences: products (records/pairs) and sums (disjoint unions/variants) correspond to conjunction and disjunction, and functions are… | ||
| Categories for the Working Hacker | Lambda Days 2018 | 2018-02-22 |
Explains how category theory models three concrete data types — products sums exponentials — and proves the specific isomorphisms like Hom(C, A×B) ≅… | ||
| Category Theory for the Working Hacker | Lambda World 2016 | 2016-09-30 |
Explains how types, logic and category theory are the same machinery by giving concrete categorical semantics for lambda calculus terms: models products and… | ||
| Propositions as Types | Lambda Days 2016 | 2016-02-25 |
Argues the concrete claim that propositions as types is an exact correspondence: formulas ↔ types, proofs ↔ programs, and normalization = evaluation, not just… | ||
| Keynote: Propositions as Types | Code Mesh 2015 | 2015-11-03 |
The principle propositions as types asserts a tight isomorphism: natural deduction ↔ typed lambda calculus, proofs ↔ programs, normalization ↔ evaluation… | ||
| Propositions as Types | Strange Loop 2015 | 2015-09-24 |
Claims that Propositions as Types means propositions are types, proofs are programs and proof normalization equals program evaluation, demonstrated by mapping… | ||
| Everything Old is New Again: Quoted Domain Specific Languages | Strange Loop 2015 | 2015-09-24 |
Claims that Quoted DSLs pair quotation with normalization to enforce the subformula property, so higher‑order host code compiles to first‑order targets… | ||
| Faith, Evolution, and Programming Languages: from Haskell to Java | Tech Mesh 2012 | 2012-12-04 |
Claims that Java generics descend from Haskell type classes and that practical adoption demands concrete engineering: a polymorphic Pizza → Java translation, a… | ||
| nothing matches | ||