WITS 2024
who it's for
language designers, compiler engineers, type system engineers, verification engineers, functional language implementers, tooling engineers, programming language researchers
topics
Scala capture checker; customizable binder syntax; Nullsafe Java plugin; application spine typechecking; heap ownership models in Dafny; generate-and-solve constraint architecture; Yaffle core for Idris 2; algebraic-effects diagnostics library; controlled definition unfolding; SMT-backed separation logic encoding
| title | author | length |
|---|---|---|
| Inside the Scala Capture Checker | Martin Odersky | 01h 03m |
Scala compiler now runs a separate pass after typing that computes and enforces capability flow: implicit capability arguments model effects, boxed generic… | ||
| Binding Syntax for Dependently-Typed Programs | Andre Videla | 25m |
Proposal adds customizable binder syntax to dependently-typed code, implemented in the Idris compiler as a fixed-grammar desugaring that desugars to lambda… | ||
| Retrofitting Null-Safety into Java | Artem Pianykh | 36m |
A compiler plugin called Nullsafe extends Java’s type system, retyping millions of lines at Meta and integrating into CI so a full retype-check runs in about… | ||
| Type inference for application spines | Simon Peyton Jones | 34m |
Argues that typechecking whole application spines — head plus all arguments — yields concrete wins: clearer error locations (e.g. “third argument of f”)… | ||
| On Modelling Heap Invariants for Type Systems in Dafny | James Noble, Tobias Wrigstad | 29m |
Claims that a middle-level heap model can express ownership-style invariants and that Dafny can both encode and check them. Builds a prototype ~500 lines of… | ||
| Solving constraints during type inference | Simon Peyton Jones | 33m |
GHC implements Pottier and Rémy’s generate-and-solve architecture: a constraint generator that walks the syntax tree and a smaller, subtler solver that… | ||
| Yaffle: A New Core for Idris 2 | Edwin Brady | 31m |
Yaffle is a new core for Idris 2 implemented in Idris 2 itself, built to fix core bottlenecks and simplify checking. It compiles via Chez Scheme and bootstraps… | ||
| asai: a Library for Compiler Diagnostics | Kuen-Bang Hou (Favonia), Reed Mullanix | 33m |
asai is an OCaml library that generates structured and partly‑unstructured compiler diagnostics, using algebraic effects to build semantic, user‑level… | ||
| Efficient Evaluation with Controlled Definition Unfolding | András Kovács | 29m |
Proposes an evaluator-for-elaboration that preserves definition unfoldings by representing top-level names as delayed top-level unfolding nodes in the semantic… | ||
| Implementing separation logic using an SMT-backed Frame Rule | Kirill Golubev, Alcides Fonseca | 22m |
Implements an SMT-backed Frame Rule by encoding a decidable fragment of separation logic into CVC5 and integrating it into Liquid Java for symbolic execution… | ||
| nothing matches | ||