~/talks

Ambroise Lafont

what they talk about

where they keep going back

no series more than once — all 3 in the filters

on a stage with

all 8 in the filters

who talks about the same things

titleconferencedate
2-Functoriality of Initial Semantics, and ApplicationsICFP 20252025-10-12
Shows that initial semantics, when parametrized by the monoidal category of contexts, is 2-functorial: a monoidal functor or adjunction between base categories…
Talk on
A diagram editor to mechanize categorical proofsCoqPL 20242024-01-20
A diagram editor runs as a web app or Electron desktop app and hooks into Coq via VS Code + coq-lsp integration, showing diagrammatic goals as graphics and…
Talk on
Dargent: A Silver Bullet for Verified Data Layout RefinementPOPL 20232023-01-15
Dargent provides a declarative layout language integrated into Cogent that generates verified C getters and setters so algebraic types map to bit-precise…
Talk
~/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.