TyDe 2020
who it's for
dependently typed language researchers, proof assistant developers, language implementers (Idris/Agda), type theory researchers, compiler engineers, macro system designers, programming language tool authors
topics
runtime proof search and exploration; Mtac2 telescope lifting; type-aware hygienic macros; symbolic holes encoded in LLVM IR; shallow presheaf embeddings of type theories; graded modal dependent types; equality-by-normalization modulo equations; later modality and guarded recursion; implicit grade inference; admit-driven execution pipeline
| title | author | length |
|---|---|---|
| Developing a Dependently Typed Language with Runtime Proof Search | Mark Lemay, Cheng Zhang, William Blair | 18m |
Prototype implements a call-by-value dependently typed language that delays constraint solving by adding an admit syntax and a three-stage pipeline: light type… | ||
| Generalization of meta programs with dependent types in mtac2 with mtac2 | Ignacio Tiraboschi, Tiraboschi et al., Jan-Oliver Kaiser, Beta Ziliani | 24m |
Presents a concrete tool that automatically transforms meta-functions to expose dependent arguments: lift analyzes a function’s signature (via a ty tree) and… | ||
| Predictable macros for hindley milner | Langston Barrett, David Thrane Christiansen, Samuel Gélineau | 20m |
Klister is an ML‑like prototype language that implements type-aware hygienic macros written in the full language (macros run in a monadic macro context) and… | ||
| Retrofitting Symbolic Holes to LLVM IR | Bruce Collie, Michael F. P. O'Boyle | 22m |
Implements untyped symbolic holes inside LLVM IR by encoding holes as calls to uninterpreted functions and introducing an unknown-type marker whole.t, plus… | ||
| Shallowly embedding type theories | Joris Ceulemans, joris kulemans, Dominique Devriese | 25m |
Library in Agda implements a shallow embedding of object type theories as presheaf models parameterized by a small base category, representing… | ||
| Towards Graded Modal Dependent Types | Benjamin Moon, Harley D. Eades III, Dominic Orchard | 20m |
Graded Modal Dependent Type Theory (GrTT) defines dependent types indexed by a preordered semiring of grades to track resource use both at runtime and in… | ||
| Frex: indexing modulo equations with free extensions (Extended Abstract) | Guillaume Allais, Edwin Brady, Ohad Kammar, Jeremy Yallop | 27m |
An extensible Idris2 library implements equality-by-normalization for indices using free extensions, with a user tier (frexlets) and a developer tier (core… | ||
| nothing matches | ||