Keynote – Edwin Brady
summary
A tour of Idris 2 shows concrete changes: a Scheme backend that compiles in an afternoon and runs faster than Idris 1, an internal “generate definition” proof-search tool that fills holes automatically, and quantitative type theory that tracks zero/one/dontcare multiplicities so values are erased or enforced at runtime. Examples include linear resource tracking (files, a “door” state machine), lightweight session types, and a clean pipeline that lowers to a QTT IR with zero multiplicities erased; performance is competitive with GHC, with Chicken/Racket trade-offs.
AI-written summary · about
chapters (4)
related talks
43mIdris 2: Type-driven development of Idris
01h 29mKeynote
41mPrograms and Proofs — Dependent Typing as a Way to Structure Your Code
58mPanel discussion: Types for All: From weak to strong, from static to dynamic
39mDependent Type Driven Program Synthesis in Idris
31mYaffle: A New Core for Idris 2
55mKeynote: Functionalist programming language design
12mIdris2-Table: Evaluating dependently-typed tables with... (Extended Abstract)