HATRA 2025
who it's for
programming language researchers, type system implementers, compiler engineers, proof assistant developers, verification engineers, Rust compiler contributors
topics
P4 mechanized specification; algorithmic inference rules; Wasm-SpecTec meta language; bidirectional type highlighting; gradually typed Hazel; liquid types usability issues; negative trait bounds for Rust; trait conflict detection algorithm; imperative-to-Idris elaboration; graphical gestural proofs for ITPs
| title | author | length |
|---|---|---|
| P4-SpecTec: A Language Mechanization Framework for P4 | Jaehyun Lee, Seokhun Jeong, Sukyoung Ryu | 25m |
P4-SpecTec defines a computable specification model for P4 using algorithmic inference rules (a constrained Wasm-SpecTec–style meta language), mechanizes… | ||
| Decomposable Type Highlighting for Bidirectional Type and Cast Systems | Max Carroll, Patrick Ferris, Anil Madhavapeddy | 27m |
Defines a formal, decomposable highlighting method that computes synthesis slice and analysis slice answers for bidirectional typing, attaches those slices to… | ||
| Types as a Specification Language for Creativity | Youyou Cong | 24m |
Proposes a typed creative language where types carry an optional refinement with two predicates: hard rules and soft rules and the typing judgment returns a… | ||
| Usability Barriers for Liquid Types (Summary of Published Work) | Catarina Gamboa, Abigail Elena Reese, Alcides Fonseca, Jonathan Aldrich | 23m |
Study of 19 developers (12 new to LiquidHaskell, 7 experienced) identifies nine concrete barriers across three themes: verification, developer experience, and… | ||
| Negative Bounds for Avoiding Conflicts in Implementing Traits in Rust | Yuki Okamoto, Isao Sasano | 22m |
Introduces negative bounds (a minus operator on trait bounds) and a detection algorithm that checks unified type params plus the overlap of positive and… | ||
| Imperative Syntax for Dependent Types | Bhakti Shah, Edwin Brady | 24m |
Claim: an imperative surface syntax that elaborates into Idris makes dependently typed code more comprehensible for experienced imperative programmers. Built… | ||
| Actema: Integrating Graphical Proofs into ITPs via Plugin-Driven Gestural Interaction | Pablo Donato, Benjamin Werner | 24m |
Actema is a prototype GUI that integrates with Rocq via a client-server plugin and exposes a web frontend (JS) and OCaml backend to build proofs by click and… | ||
| nothing matches | ||