TyDe 2025
who it's for
type system researchers, dependently typed programmers, programming language designers, functional programmers, programming language tool developers, proof assistant engineers
topics
typed prompt calculi; prompt constraint enforcement; Hazel corpus generation from OCaml; translation using typed holes; BST and AVL correctness-by-construction; type-level naturals for keys; unification modulo type isomorphisms; constraint-based generation of well-typed programs; normalization-by-evaluation performance comparison; opaque definitions in dependent type theory; conatural numbers in Cubical Agda; gradual metaprogramming with quote coercions
| title | author | length |
|---|---|---|
| Type-Driven Prompt Programming: From Typed Interfaces to a Calculus of Constraints | Abhijit Paul | 28m |
Survey of 15 recent works finds type systems recurring in prompt frameworks and presents a formal proposal called lambda Prompt, a dependently typed calculus… | ||
| Generating a corpus of Hazel programs from ill-typed OCaml programs | Patrick Ferris, Anil Madhavapeddy | 25m |
A compiler translates OCaml programs into Hazel, producing a large corpus of both well‑typed and ill‑typed Hazel code by reusing OCaml packages and an… | ||
| Representing Data Structures with Invariants in Haskell: the cases of BST and AVL | Nicolas Rodriguez, Alberto Pardo, Marcos Viera | 29m |
Three concrete encodings for BSTs and AVLs in Haskell are implemented and compared: a proof-paired EBST paired with proof that stores a separate inductive… | ||
| Unification Modulo Isomorphisms between Dependent Types for Type-based Library Search | Satoshi Takimoto, Sosuke Moriguchi, Takuo Watanabe | 29m |
Claims an equational unification procedure modulo a set of type isomorphisms for dependent product/sum types and presents a semi-algorithm plus a prototype… | ||
| Constrained generation of well-typed programs | Hugo Barreiro, Gabriel Scherer | 30m |
Approach reuses constraint-based type inference (Pottier & Rémy style) by parameterizing constraint generation over a search monad, representing partial… | ||
| Towards a Performance Comparison of Syntax and Type-Directed NbE | Chester Gould, William J. Bowman | 23m |
Implements a forked Smalltt to add a type-directed judgmental-equality procedure and compares it against Andreas Kovác’s syntax-directed Smalltt using… | ||
| A Formalization of Opaque Definitions for a Dependent Type Theory | Nils Anders Danielsson, Eve Geng | 24m |
Formal development of top-level opaque definitions is mechanized in Agda and proves that adding opacity preserves subject reduction, normalization, consistency… | ||
| The conatural numbers form an exponential commutative semiring | Szumi Xie, Viktor Bense | 30m |
Claims a first mechanized proof that conatural numbers form an exponential commutative semiring in cubical type theory by formalizing addition, multiplication… | ||
| Gradual Metaprogramming | Tianyu Chen, Darshal Shetty, Jeremy G. Siek, Chao-Hong Chen, Weixi Ma, Arnaud Venet, Rocky Liu | 31m |
A calculus called MetaGTLC models a gradually typed metalanguage that generates statically typed object code and compiles to an explicit cast calculus MetaCC… | ||
| nothing matches | ||