~/talk

A Lazy, Concurrent Convertibility Checker

on YouTube 25m
Talkat POPL 2026 · 2026-01-11..01-17· [compilers-and-language-design]

speakers

name:Nathanaëlle Courant
links:none on file
name:Xavier Leroy
links:none on file

resources

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

summary

A convertibility algorithm that interleaves evaluation and comparison using lazy channels and concurrent processes, representing lazy values as channels and forcing as waits, so identical subcomputations are shared and different unfoldings are explored in parallel. It uses short-circuiting choice and a bias choice operator to stop as soon as a subproof decides, avoids redundant constant unfolding, and provides an explicit scheduler. Mechanized partial correctness proof and artifacts are available; worst-case complexity is exponential in the shortest-proof size but is near-linear in the authors’ experiments.

AI-written summary · about

chapters (24)

  1. 0:00Introduction to the talk
  2. 0:21Speaker introduction and motivation
  3. 1:03Why lazy evaluation matters for convertibility
  4. 2:34Drawbacks of existing convertibility strategies
  5. 4:23Formal problem statement and assumptions
  6. 5:26Textbook and standard convertibility tests
  7. 6:31Proposal for a concurrent convertibility checker
  8. 7:16Process calculus for lazy evaluation
  9. 9:07Concurrent convertibility test definition
  10. 10:11Weak head normal forms in the process model
  11. 11:15Pure lambda calculus convertibility rules
  12. 12:40Concurrent stack comparison and short-circuiting
  13. 13:25Handling constants in convertibility
  14. 14:54Bias choice operator for constant unfolding
  15. 15:36Complexity analysis and theoretical guarantees
  16. 16:44Formalization and correctness proof
  17. 17:28Additional optimizations and extensions
  18. 18:33Explicit scheduling algorithm
  19. 19:15Conclusion and future work
  20. 20:09Q&A: Exponential optimality gap
  21. 20:52Q&A: Relation to non-deterministic algorithms
  22. 21:54Q&A: Comparison with Coq's convertibility
  23. 22:58Q&A: Applicability to unification solvers
  24. 23:41Q&A: Efficiency vs breadth-first search

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.