ML 2021
who it's for
ocaml developers, functional language researchers, language implementers, type system researchers, proof assistant engineers, formal verification engineers, compiler engineers
topics
effect handlers for UNIX; deductive verification for OCaml; contextual equivalence checking; OCaml GADT typing in Coq; verified lexer generation; Coq to ML code extraction; F# domain modeling practices; multi-phase modularity metalanguage; unfolding ML datatype declarations; frozen inference constraints; library search up to isomorphism; typed notation for symbolic mathematics
| title | author | length |
|---|---|---|
| Composing UNIX with Effect Handlers: A Case Study in Effect Handler Oriented Programming | Daniel Hillerström | 25m |
Implements a miniature UNIX in Links using algebraic effect handlers: defines a write operation and a basic_io handler that returns the accumulated file as a… | ||
| Cameleer: a Deductive Verification Tool for OCaml | Mário Pereira, António Ravara, antonio rivara | 28m |
Cameleer takes OCaml source annotated with Gospel specs, translates the AST to Why3 and emits VCs solved by SMTs (demo uses Alt-Ergo); it targets core OCaml… | ||
| Hobbit: A Tool for Contextual Equivalence Checking Using Bisimulation Up-to Techniques | Vasileios Koutavas, Yu-Yang Lin, Nikos Tzevelekos | 20m |
Hobbit is a bounded model checker that verifies contextual equivalence for higher-order programs with local state by combining symbolic environmental… | ||
| Formalizing OCaml GADT typing in Coq | Jacques Garrigue, Xuanrui Qi | 24m |
Mechanization of OCaml GADT typing in Coq formalizes ambivalent-type principality and proves subject reduction for a graph-based encoding; implementation… | ||
| Demo Paper : Coqlex, an approach to generate verified lexers | Wendlasida Ouedraogo, Danko Ilik, Lutz Strassburger | 23m |
Coqlex generates lexers in Coq from a list of regular expressions plus actions, proves correctness of the regex engine, match/score computation and lexer… | ||
| Code Extraction from Coq to ML-like languages | Danil Annenkov, Mikkel Milo, Bas Spitters | 24m |
Pipeline implemented wholly in Coq uses MetaCoq's verified erasure to produce a typed intermediate lambda-box-t representation, runs a certifying preprocessing… | ||
| Keynote: Narratives and Lessons from The Early History of F# | Don Syme, Jon Harrop | 01h 24m |
Covers why F# keeps the core OCaml experience: start with OCaml-like syntax and type inference, run on the .NET VM for generics and performance, and trade some… | ||
| A metalanguage for multi-phase modularity | Jonathan Sterling, Robert Harper | 16m |
Proposes a metalanguage that lets the compiler inline representations without breaking programmer abstractions by indexing types and judgments in a phase… | ||
| Unfolding ML Datatype Declarations Without Loops | Nicolas Chataing, irene m gabriel, Gabriel Scherer, nicolas châtain | 24m |
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 | Olivier Martinot, Gabriel Scherer | 28m |
Presents a method for disambiguating overloaded names in statically typed languages by recording ‘frozen’ type inference constraints during compilation. Uses… | ||
| Experience Report: Domain Modeling with F# (short talk) | Scott Wlaschin | 13m |
Argues that F# serves as a practical replacement for COBOL/Java for business domain modeling by using algebraic types, single‑case unions and smart… | ||
| Isomorphisms are back! (short talk) | Clément Allain, Gabriel Radanne, Laure Gonnord | 11m |
A library search tool called dowsing finds functions up to type isomorphism (tuples commutative/associative, unit neutral, currying) and keeps soundness and… | ||
| Sylvester: Unified, typed, notation for symbolic mathematics and proofs (short talk) | Allister Beharry | 14m |
Claim: F# becomes a single interactive language that unifies computer algebra and theorem proving. Built is the Sylvester library running in Jupyter/VS Code… | ||
| A Data-centered User Study for jsCoq (short talk) | Hanneli Tavante | 10m |
A lightweight data pipeline records every interaction with a modified jsCoq front end inside Docker Compose, sends click and shortcut events to a Node.js event… | ||
| Full Workshop | Jonathan Protzenko, Martin C̅er̅n̅ek, Daniel Hillerström | 07h 18m |
A fast tour of research tools and case studies from ML 2021: a running effect-handler Unix model that composes write/exit/su/fork/interrupt handlers and… | ||
| nothing matches | ||