Summer research thoughts & near future projects:
- NS proof term decompiler (ongoing)
- DTT for ML (planning, need interested students)
- e-graphs for automatic transport in cubical (planning, need interested students)
- reifying semantics as syntax for NS proof search (thinking)
Conversation
NS = neurosymbolic
DTT = dependent type theory
ML = machine learning (in this particular context)
cubical = cubical type theory
2
2
Also have room for lots of work continuing along the proof repair line, and want to do some more mixed-methods verification work using that. Will plan that in July. Have capacity for 1-2 Ph.D. students who care about proof automation. Plus 1-2 with any overlapping interests
1
4
You'll like working with me if you think types are beautiful, but you want them to be both beautiful and useful, and you think the way to do that is to build good automation and user experience, meeting software engineers where they are
2
1
10
Or if you think that, in an ideal world, formal proof about program correctness really shouldn't be much harder than writing unit tests
2
1
9
If you're generally not afraid of ideas that tread totally new ground, and if you think most things that are hard are only hard because we haven't worked on them enough yet, not because they ought to be hard
2
1
8
Replying to
This is a big part of what I hope we can improve with type theory-based programming tools (and learning how to build tools based on type theory). I strongly believe we can and should work on reducing the barrier to entry in order to help people everywhere.