HATRA 2024
who it's for
programming language researchers, proof assistant developers, programming education researchers, language tool developers, program synthesis researchers, compiler and tooling engineers, Python developers
topics
dynamic gradual typing; mypy any usage patterns; automatic any fixes; library learning for Python; AST extraction and Stitch; macro-like fragment detection; abstraction-based program compression; classroom proof assistant design; structure editor metatheory proofs; live gradual structure-editing UI; automated proof search modes; induction and hypothesis tooling
| title | author | length |
|---|---|---|
| Toward a Corpus Study of the Dynamic Gradual Type | Dibri Nsofor, Ben Greenman | 33m |
Corpus analysis targets 221 mypy-annotated GitHub projects and finds roughly 320,000 any occurrences, then clusters them into eight patterns of use. Several… | ||
| Leroy: Library Learning for Imperative Programming Languages | Abhiram Bellur, Razan Alghamdi, Kidus Workneh, Joe Izraelevitz | 20m |
Leroy converts Python programs to a lisp-like AST and runs Stitch to extract repeated fragments, then prunes and patches candidates back into valid Python… | ||
| Learner-Centered Design Criteria for Classroom Proof Assistants | Matthew Keenan, Cyrus Omar | 26m |
Survey synthesizes classroom reports into actionable design rules: error messages must be clear, local, and show which premises are correct (green feedback for… | ||
| Don’t Call Us, We’ll Call You | Jan Liam Verter, Tomas Petricek | 32m |
A small prototype proof assistant implements two modes: auto-search-first where the tool runs an automated search and halts to ask for user feedback, and… | ||
| Research Methods for Designing Next-Generation Programming Systems | Cyrus Omar | 01h 32m |
Claims a structure editor called Hazel makes every edit state syntactically, statically and dynamically well defined, with mechanized Agda proofs (a “cat… | ||
| nothing matches | ||