Jeremy Yallop
where else to find them
what they talk about
where they keep going back
all 8 in the filters
on a stage with
all 27 in the filters
who talks about the same things
- Gabriel Scherer12 talks
- Ningning Xie21 talks
- Stephen Dolan13 talks
- Yizhou Zhang13 talks
- Nicolas Wu25 talks
- Nada Amin26 talks
| title | conference | date |
|---|---|---|
| Handling Scope Checks: A Comparative Framework for Dynamic Scope Extrusion Checks | POPL 2026 | 2026-01-11 |
Compares three concrete dynamic checks—lazy vs eager and a new Cause-for-Concern (C4C) check—and gives a formal calculus for evaluating them with effect… | ||
| Typed Abstractions for Causal Probabilistic Programming | LAFI 2026 | 2026-01-11 |
A Haskell library reimplements Cairo’s causal features with concrete types, extracting a cosmonad (a reader monad transformer over a probability monad) to… | ||
| Brack: A Verified Compiler for Scheme via CakeML (Lightning Talk) | Scheme 2025 | 2025-10-16 |
Brack is a verified compiler for Scheme implemented in HOL4 that compiles a small subset (lambdas, lists, mutation) to ML and leans on CakeML to get down to… | ||
| TEAL: a Total Expressive Assembly Language | VMIL 2025 | 2025-10-15 |
Design of a typed assembly language called TEAL claims total correctness: well-typed programs both terminate and return the specified source-level value. The… | ||
| Safe Pattern Generation for Multi-Stage Programming | ML 2024 | 2024-09-06 |
Design for typed generation of patterns whose shape is only known at staging time, implemented as a library on Metro camel. Core techniques are inductive code… | ||
| Unboxed data constructors -- or, how cpp decides a halting problem | POPL 2024 | 2024-01-14 |
Adds selective unboxing to OCaml with a prototype compiler and a static check that rejects unboxings that would create overlapping representations, yielding up… | ||
| MacoCaml: Staging Composable and Compilable Macros | ICFP 2023 | 2023-09-04 |
MacoCaml implements compile‑time code generation inside the OCaml compiler, treating macros as compile-time bindings and using quotation/splice staging so… | ||
| Modular Construction of Multi-sorted Free Extensions | PEPM 2023 | 2023-01-16 |
Defines how to build combined free extensions by composing existing frexes and gives three modular constructions: a concrete involutive algebra frex (covers… | ||
| Normalization by Evaluation with Free Extensions (Extended Abstract) | TyDe 2022 | 2022-09-11 |
Claim: augmenting normalization-by-evaluation with free extensions (frex) produces a single generic NbE algorithm for simply typed lambda calculus with… | ||
| Staging with Class: A Specification for Typed Template Haskell | POPL 2022 | 2022-01-16 |
Shows that Template Haskell’s interaction with overloading is unsound: splicing well-typed code can produce missing-dictionary errors. Proposes staged type… | ||
| A Practical Mode System for Recursive Definitions | POPL 2021 | 2021-01-17 |
A static mode system that classifies recursive bindings as safe or vicious and is proven sound against the Nordlander–Carlsson–Gill source semantics. It gives… | ||
| Frex: indexing modulo equations with free extensions (Extended Abstract) | TyDe 2020 | 2020-08-23 |
An extensible Idris2 library implements equality-by-normalization for indices using free extensions, with a user tier (frexlets) and a developer tier (core… | ||
| nothing matches | ||