TyDe 2023
who it's for
programming language researchers, dependently typed language implementers, proof assistant developers, programming language tool builders, quantum programming language researchers, functional programming language designers
topics
applicative functor phase fusion; Day convolution phases; inductive linear constructions; dynamic equality with casts; graded dependent linear types; infix-extensible record types; probabilistic programming in Coq; dependent types for feature engineering; type-theoretic quantum circuits in Coq; modal types for Intel Quantum SDK; linking types for foreign code; types-as-values in Fuzion
| title | author | length |
|---|---|---|
| Multi-phase computation as an applicative functor | Jeremy Gibbons, Donnacha Oisín Kidney, Tom Schrijvers, Nicolas Wu | 01h 18m |
Claims that structuring a computation as an applicative with phases (implemented via Day convolution / an iterated, homogeneous “phases” type) lets a single… | ||
| A Calculus of Inductive Linear Constructions | Qiancheng Fu, Hongwei Xi | 22m |
A new calculus combines linear and dependent types with inductive typing schemes and a guarded fixpoint plus case instead of ordinary induction for linear data… | ||
| A Dependently Typed Language with Dynamic Equality | Mark Lemay, Qiancheng Fu, William Blair, Cheng Zhang, Hongwei Xi | 19m |
Designs a dependently typed language that defers equality checking to runtime and replaces many static rejections with warnings, inserting explicit casts and… | ||
| Combining Dependency, Grades, and Adjoint Logic | Peter Hanukaev, Harley D. Eades III | 19m |
Two new dependent type systems appear: a graded dependent/linear system that links graded usage annotations (from a semiring) to a linear fragment via modal… | ||
| Infix-Extensible Record Types for Tabular Data | Adam Paszke, Ningning Xie | 18m |
A row-polymorphic record calculus that adds scoped labels and first-class labels and rows plus record concatenation, with a Hindley-Milner–style inference… | ||
| An Intrinsically-typed Probabilistic Programming Language in Coq (Extended Abstr... | Ayumu Saito, Reynald Affeldt | 24m |
Mechanization in Coq of an intrinsically-typed first-order probabilistic language with a denotational semantics that returns measures and proves measurability… | ||
| A Type System For Feature Engineering (Extended Abstract) | Weixi Ma, Serena Chan, Fei Yu | 22m |
Built a small compiler for F3-style SQL DSL at Meta and demonstrates a dependent type system (inspired by Martin-Löf) that stores normal forms to make… | ||
| A type-theoretic account of quantum computation (Extended Abstract) | Takafumi Saikawa, Jacques Garrigue | 28m |
Provides a Coq encoding of pure quantum circuits that represents states as functions and transformations as parametric, natural linear maps, requires proving… | ||
| Exploring modal types for the Intel Quantum SDK (Extended Abstract) | Jennifer Paykin | 23m |
Defines a modal type system for the Intel Quantum SDK that enforces the SDK rule that every quantum kernel compiles to at most one quantum basic block, using… | ||
| Semantic Encapsulation using Linking Types | Daniel Patterson, Andrew Wagner, Amal Ahmed | 26m |
Presents a concrete mechanism that lets a pure language safely link to foreign code by adding linking types that describe C‑like behaviors, proving soundness… | ||
| Towards Tagless Interpretation of Stratified System F (Extended Abstract) | Peter Thiemann, Marius Weidner | 19m |
An intrinsically typed, tagless interpreter for a stratified fragment of System F is formalized in Agda: types carry natural-number levels and map to Set_l so… | ||
| Types as First-Class Values in Fuzion (Extended Abstract) | Fridtjof Siebert | 26m |
Fuzion is a prototype language that treats types as compile-time values and unifies type and value arguments so calls accept explicit type parameters; it adds… | ||
| Pipit: Reactive Systems in F★ (Extended Abstract) | Amos Robinson, Alex Potanin | 18m |
Pipit is a small embedded DSL in F★ that implements reactive streams with Follow by delays and guarded recursion, provides a verified translation to transition… | ||
| nothing matches | ||