Student Research Competition Final Presentations
summary
Session collects six short student projects with concrete artifacts and techniques: HenBlocks: structured editing for Coq is a client‑side web app (GS‑Coq front end) that guarantees syntactically valid proofs, offers drag‑drop tactic blocks, context dropdowns and auto‑renaming; compiling Hazel with holes targets Grain/WASM, defines a compact runtime layout for indeterminate results, and a static three‑way completeness analysis plus embedding/projection casts; graph‑typed futures adds vertex streams to permit recursive lists of futures and produces graph types for spawn/touch patterns; a categorical account of generalised free extensions gives a universal‑property correctness for dependent‑operation normal forms; constraint‑based inference work produces an executable, ITC‑style monadic interface with predicate‑transformer proofs and role/world indexing for scoped unification; a Coq‑formalised lazy abstraction model checker implements a fuelled transition system, currently using SMT oracles with a path toward validator integration.
AI-written summary · about