TyDe 2019
who it's for
programming language researchers, dependently typed programmers, proof assistant developers, language tool builders, editor and tooling engineers, programming language compiler engineers, functional programmers
topics
typed holes with live evaluation; Hazel editor node staging; shifted names representation; Coq formalization of CPS; dependent type Tic-Tac-Toe; length-indexed vectors; sequential decision processes in Agda; monadic probabilistic generalisation; Agda reflection for tactics; proof-delay applicative in Trip; live literals with GUI expansion
| title | author | length |
|---|---|---|
| Flexible Structure Editing of Well-Typed Expressions | David Moon, Cyrus Omar, Ben Shapiro | 19m |
Hazel enforces that every edit state is syntactically, statically and dynamically well-defined by combining typed holes with execution semantics that evaluate… | ||
| Syntax with Shifted Names | Stephen Dolan, Leo White | 21m |
Claims a new representation called shifted names that tags free names with numeric indices so freshness side-conditions disappear. Defines four concrete… | ||
| Tic Tac Types | Sean Innes, Nicolas Wu | 15m |
Implements Tic‑Tac‑Toe with dependent types: starts from unsafe |String| boards, moves to vectors that know their length, then encodes moves as data… | ||
| An Algebra of Sequential Decision Problems | Robert Krook, Patrik Jansson | 17m |
Formalises sequential decision processes in Agda and implements reusable composition primitives, claims small three combinators let one-dimensional step… | ||
| Monadic typed tactic programming by reflection | Liang-Ting Chen | 25m |
Shallow embedding of Mtac is implemented entirely in Agda by reusing Agda reflection and quotations to represent tactic terms as Agda syntax; the… | ||
| Deferring the Details and Deriving Programs | Liam O'Connor | 18m |
Claims a proof-delay applicative that moves embedded proof terms out of data and program ASTs, implemented in Trip inside Agda. Builds a verification-condition… | ||
| Livelits: Filling Typed Holes with Live GUIs | Cyrus Omar, Nick Collins, David Moon, Ian Voysey, Ravi Chugh | 20m |
Introduces live literals that let a GUI fill typed holes and expand to code via an explicit expand function; implemented in the Hazel editor using a… | ||
| nothing matches | ||