TyDe 2024
| title | author | length |
|---|---|---|
| Towards Type-Directed API Search for Mainstream Languages | Marc Etter, Farhad D. Mehta | 27m |
Claims a proof-search-based engine that treats types as specifications, supports first-class subtyping and parametric polymorphism, and translates library… | ||
| Term Search in Rust | Tavo Annus, Philipp Joram | 20m |
Term Search in Rust (Video, TyDe 2024)
Tavo Annus and Philipp Joram
(Tallinn University of Technology, Estonia; Tallinn University of Technology… | ||
| Typed, Concise, Nanopass (pick 3) (Extended Abstract) | Lawrence Chonavel | 23m |
Shows how to get a typed, concise, nanopass compiler by replacing recursive lists with a custom indexed args type and a single generic map traversal, moving… | ||
| Normalizable types | Stefan Monnier | 23m |
Proposes an adjusted normalized-quotient design that separates typechecking and runtime reduction so canonicalization runs only during checking and is erased… | ||
| First-class Algebraic Presentations with Elaborator Reflection (Extended Abstract) | Robert Wright, Ohad Kammar | 20m |
Library for Idris 2 that reinterprets fragments of host syntax at compile time to give user-definable deeply embedded many-sorted algebras without changing… | ||
| Modal Mu-Calculus for Free in Agda | Ivan Todorov, Casper Bach Poulsen | 20m |
Embeds the modal μ-calculus into Agda by representing possibly nonterminating effectful programs as a coinductive free monad encoded with coinductive records… | ||
| Type-level Property Based Testing | Thomas Ekström Hansen, Edwin Brady | 20m |
An automated framework in Idris 2 runs type-level QuickCheck during compilation to test dependent-type models built as an indexed state monad. Properties… | ||
| How Novices Perceive Interactive Theorem Provers (Extended Abstract) | Sára Juhošová | 23m |
Survey of 35 bachelor students who learned Agda for two weeks finds five concrete obstacles: unfamiliar concepts (dependent types and proof-centric workflow)… | ||
| Dependent Types to Push Corners of the Property-based Testing (Extended Abstract) | Denis Buzdalov | 21m |
Generates dependently-typed inputs from Idris specifications to fuzz a TypeScript-like compiler and interpreter, using a partly derived dep_check library… | ||
| A Type- And Control- Flow Analysis for System FC (Extended Abstract) | Skye Soss, John Reppy | 22m |
Presents a higher-order control- and type-flow analysis that handles System FC coercions and witnesses by extending standard CFA bookkeeping to track… | ||
| nothing matches | ||