~/talk

Frex: Free Extensions for Normalization-by-Evaluation

on YouTube 35m
Talkat PEPM 2020 · on Monday, 2020-01-20· [compilers-and-language-design]

speaker

name:Ohad Kammar
links:none on file

resources

video:https://youtu.be/0ps0CJH2Dd8
slides:none on file

summary

Frex is a library that constructs free extension semantic domains to get normalization by evaluation for arbitrary algebraic theories; it ships solver specs for common structures (e.g. a commutative monoid) and is extensible so users add solvers for new operations. Implementations exist in Haskell and experimental Idris code; using it for partial evaluation yields a provable speedup (linear win in a staged matrix-multiply example) and produces sound, complete normal forms to unblock unification in type-checked modular equations, though the type-checker integration is work in progress.

AI-written summary · about

chapters (6)

  1. 0:00Start
  2. 3:50Indexing Modular Equations
  3. 5:20Define Alternating Lists
  4. 9:06Algebraic Laws
  5. 18:39What Is the Free Extension
  6. 29:25Summary

related talks

~/search
type to search 6,249 conferences, 138,987 speakers and 185,172 talks
~/help
cmdctrl k
search every conference, speaker and series
/
focus the filter search
h
home
c
conferences
s
speakers
e
series
t
light / dark — the status bar button does the same
?
this help
esc
close this, then clear every filter — or just the search, while you are typing in it

Ignored while you are typing. Pages without a filter rail have no search to focus.