Jeremy G. Siek
where else to find them
what they talk about
all 5 in the filters
where they keep going back
- PLDI Workshop Honoring Andreas Podelski2 editions2022–2024
all 5 in the filters
on a stage with
all 12 in the filters
who talks about the same things
- Matthias Felleisen10 talks
- Éric Tanter12 talks
- Philip Wadler14 talks
- Tiark Rompf24 talks
- Jan Vitek26 talks
- Steve Zdancewic19 talks
| title | conference | date |
|---|---|---|
| Gradual Metaprogramming | TyDe 2025 | 2025-10-12 |
A calculus called MetaGTLC models a gradually typed metalanguage that generates statically typed object code and compiles to an explicit cast calculus MetaCC… | ||
| Quest Complete: The Holy Grail of Gradual Security | PLDI 2024 | 2024-06-24 |
Claims a language 𝜆★IFC that satisfies both noninterference and the gradual guarantee by removing the unknown label ★ from runtime security labels, keeping… | ||
| Deep and Shallow Types for Gradual Languages | PLDI 2022 | 2022-06-13 |
Combines deep (natural) and shallow (transient) gradual typing into one language and proves they interoperate while preserving deep’s type soundness and… | ||
| Extrinsically Typed Operational Semantics for Functional Languages | SLE 2020 | 2020-11-16 |
Lang-n-check automates checking of language specifications by taking an extrinsically typed operational semantics and verifying that typing rules and reduction… | ||
| Optimizing and Evaluating Transient Gradual Typing | DLS 2019 | 2019-10-20 |
Gradual typing for Python via Reticulated Python inserts many lightweight runtime checks and shows up to a 6× slowdown on CPython as programs go from dynamic… | ||
| Theory & Models of Lambda Calculus: Typed and Untyped (Part 6) | LambdaConf 2018 | 2018-06-03 |
Claims a concrete model: using the powerset of the integers with enumeration operators to model application, abstraction and computability, then adds a… | ||
| Theory & Models of Lambda Calculus: Typed and Untyped (Part 5) | LambdaConf 2018 | 2018-06-03 |
Model uses the powerset of N with enumeration operators to model application and abstraction; closure operators correspond to subspaces and fixed points equal… | ||
| Theory & Models of Lambda Calculus: Typed and Untyped (Part 3) | LambdaConf 2018 | 2018-06-03 |
Presents a concrete model: represent data as subsets of N and functions as enumeration operators on P(N) so application becomes a lookup-table operation on… | ||
| Theory & Models of Lambda Calculus: Typed and Untyped (Part 3) | LambdaConf 2018 | 2018-06-03 |
Claims a concrete model of lambda calculus built on the powerset of the integers, using enumeration operators as the actual implementation of application and… | ||
| Theory & Models of Lambda Calculus: Typed and Untyped (Part 2) | LambdaConf 2018 | 2018-06-03 |
Claims a concrete semantic model: use the powerset of the integers with enumeration operators to interpret application and abstraction, and show that Church… | ||
| Theory & Models of Lambda Calculus: Typed and Untyped (Part 1) | LambdaConf 2018 | 2018-06-03 |
Shows a concrete model: application and abstraction realized by enumeration operators on P(N) with a topology, not handwavy category talk. Carries out… | ||
| Crash Course on Notation in Programming Language Theory (Part 1) | LambdaConf 2018 | 2018-06-03 |
Crash course promises concrete mechanics: reading POPL/ICFP notation by building inductive definitions with base cases and rules, drawing derivation trees… | ||
| Crash Course on Notation in Programming Language Theory (Part 2) | LambdaConf 2018 | 2018-06-03 |
Clear, hands‑on coverage of the notation you actually need: grammars for syntax, sets/tuples/relations and inductive definitions, worked big-step and… | ||
| nothing matches | ||