Scheme 2025
2025-10-16
Singapore, Singapore
Scheme ·
[Scheme 2019, Scheme 2020, Scheme 2021, Scheme 2022, Scheme 2023, Scheme 2024, Scheme 2025, Scheme 2026]
who it's for
language designers, compiler engineers, Scheme implementers, Racket developers, verification engineers, Rust developers, programming language researchers
topics
staged environment machines; hygienic procedural macros; micros syntax-to-IR embeddings; verified Scheme compiler via CakeML; Scheme in async Rust; default typing for Scheme; seven-form debug interpreter; tiny R7RS-small VM; finite-choice logic DSL; on-the-fly macro rewriting; automatic FSM invariant testing; denotational semantics in Agda
| title | author | length |
|---|---|---|
| Hygienic Macros via Staged Environment Machines (Position Paper) | Yuito Murase | 20m |
Argues that hygienic procedural macros map to a deterministic staged operational model by elaborating multi-stage alpha-renaming into an abstract staged… | ||
| Fast and Extensible Hybrid Embeddings with Micros | Sean Bocirnea, William J. Bowman | 25m |
Claims a hybrid embedding pipeline that uses micros (syntax→IR) to produce mutable Racket structures, runs transformations via attached generics, and re‑emits… | ||
| Scheme Reports at Fifty: Where do we go from here? | Daphne Preston-Kendal | 23m |
New election for the steering committee starts now: voter registration and nominations open through 15 January, voting in the first two weeks of January… | ||
| Brack: A Verified Compiler for Scheme via CakeML (Lightning Talk) | Pascal Lasnier, Jeremy Yallop, Magnus O. Myreen | 12m |
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… | ||
| Gouki Scheme: An Embedded Scheme Implementation for Async Rust | Matthew Plant | 29m |
Gouki Scheme is an R6RS implementation embedded in async Rust that compiles Scheme to CPS and JITs it (swapping LLVM for a Cranelift-style pipeline) to produce… | ||
| Sound Default-Typed Scheme (Position Paper) | Jan-Paul Ramos-Davila | 20m |
Proposes a concrete default typing system where each expression carries a plausibility-ranked set of types (rank 0 = common, rank ∞ = impossible), implemented… | ||
| Scheme and New Frontiers for Language Design | Michael D. Adams | 01h 00m |
Argues that adding a single seven-form interpreter extension — a debug statement that suspends execution and lets you inspect code, environment, store and… | ||
| Stak Scheme: The tiny R7RS-small implementation | Yota Toyama | 22m |
Stak Scheme implements a full R7RS-small system with a claimed 10 KLOC core: a bytecode compiler in 1.6 KLOC of Scheme and a 1.5 KLOC Rust VM. It supports… | ||
| miniDusa: An Extensible Finite-Choice Logic Programming Language (Lightning Talk) | Ari Prakash, Zachary Eisbach | 09m |
miniDusa implements Dusa-style finite-choice primitive logic programming as a hosted DSL using syntax-spec in Racket, compiling surface syntax to a core with… | ||
| Rewriting Macros on the Fly: A Modular Approach to Administrative Reduction During(…) | Paul Downen | 25m |
A system rewrites administrative expressions during macro expansion to avoid the extra lambdas and applications that CPS and other transforms ordinarily emit… | ||
| Automatic Invariant Testing for Finite-State Machines | Marco T. Morazán, Sophia Turano, Andrés M. Garced, David Anthony K. Fields | 20m |
Tool automatically generates unit tests for state invariants by traversing a machine’s transition relation in an FSM DSL in Racket, removing dead states, and… | ||
| Checking a Denotational Semantics of Scheme in Agda | Peter D. Mosses | 34m |
A shallow embedding of the R5RS denotational semantics into Agda is implemented and type-checked, revealing concrete well-formedness bugs (including a missing… | ||
| nothing matches | ||