~/talk

Compositional pre-processing for automated reasoning in dependent type theory

on YouTube 21m
Talkat CPP 2023 · 2023-01-16..01-17· [compilers-and-language-design]

speakers

name:Valentin Blot
links:none on file
name:Denis Cousineau
links:none on file
name:Enzo Crance
x:cranceltik
name:Louise Dubois de Prisque
links:none on file
name:Chantal Keller
links:none on file
name:Assia Mahboubi
links:none on file
name:Pierre Vial
links:none on file

resources

video:https://youtu.be/sImfouZbzf8
slides:none on file

summary

Implements compositional, small-step goal transforms for Coq that systematically convert inductives, uninterpreted symbols and higher-order/dependent constructs into fragments consumable by external solvers. The toolchain includes an orchestration called snipe orchestration, a theory-mapping plugin tract plugin and targeted preprocessors like zedify preprocessing and mc35; it produces G' plus a proof that G' implies G and successfully discharges non-inductive subgoals (examples: lambda‑calculus shift lemmas). Prototype works end‑to‑end but currently re‑saturates contexts (no caching yet).

AI-written summary · about

chapters (9)

  1. 0:00Automated reasoning intro
  2. 3:38Preprocessing challenges
  3. 5:10Example goals and Snipe tactic
  4. 6:36Inductive type preprocessing
  5. 8:52Symbol preprocessing with Tract
  6. 13:47First-order transformations
  7. 14:27Preprocessing tactic orchestration
  8. 16:55Future work on compositionality
  9. 18:24Q&A on incremental preprocessing

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.