Gabriel Scherer
where else to find them
no profile links on file
what they talk about
where they keep going back
all 4 in the filters
on a stage with
all 18 in the filters
who talks about the same things
- Jeremy Yallop12 talks
- Stephen Dolan13 talks
- Steve Zdancewic19 talks
- François Pottier14 talks
- Michael Sammler16 talks
- Michel Steuwer17 talks
| title | conference | date |
|---|---|---|
| Omnidirectional type inference for ML | WITS 2026 | 2026-01-17 |
Proposes omnidirectional type inference: constraints can suspend on unification variables and resume when shape information arrives via suspended match… | ||
| Zoo: A Framework for the Verification of Concurrent OCaml 5 Programs using Separation(…) | POPL 2026 | 2026-01-11 |
Zoo delivers a transpiler plus proof framework that translates OCaml 5 into a limited ZooLang fragment embedded via a deep embedding in Rocq, where programs… | ||
| Constrained generation of well-typed programs | TyDe 2025 | 2025-10-12 |
Approach reuses constraint-based type inference (Pottier & Rémy style) by parameterizing constraint generation over a search monad, representing partial… | ||
| Tail Modulo Cons, OCaml, and Relational Separation Logic | POPL 2025 | 2025-01-19 |
Implements Tail Modulo Constructor in the OCaml compiler and shows it reliably turns non‑tail List.map‑style definitions into stack‑safe code; proof of… | ||
| Pattern-matching on mutable values: danger! | ML 2024 | 2024-09-06 |
The OCaml pattern-matching compiler produces incorrect code in a corner case: matching on a value with mutable fields that are mutated during pattern-matching… | ||
| 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… | ||
| Boxroot, fast movable GC roots for a better FFI | ML 2022 | 2022-09-15 |
Boxroot is a C library that implements a caller-roots protocol and an allocator for one-word roots, used already by several OCaml–Rust bindings. It chooses… | ||
| An OCaml use case for strong call-by-need reduction | ML 2022 | 2022-09-15 |
Describes a concrete OCaml-compiler change: a strong call-by-need reduction strategy for the module language, implemented as an evaluator inside the compiler… | ||
| Unfolding ML Datatype Declarations Without Loops | ML 2021 | 2021-08-26 |
Presents a technique for expanding ML-style algebraic datatype declarations into fully-defined type representations without using recursive loops or explicit… | ||
| Frozen inference constraints for type-directed disambiguation | ML 2021 | 2021-08-26 |
Presents a method for disambiguating overloaded names in statically typed languages by recording ‘frozen’ type inference constraints during compilation. Uses… | ||
| 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… | ||
| nothing matches | ||