Edwin Brady
where else to find them
what they talk about
all 6 in the filters
where they keep going back
- Code Mesh LDN2 editions2018–2020
- TyDe2 editions2020–2024
all 10 in the filters
on a stage with
- Bhakti Shahonce
- Felienne Hermansonce
- Gilad Brachaonce
all 10 in the filters
who talks about the same things
- Brian McKenna6 talks
- Miles Sabin13 talks
- Ian Dees4 talks
- Stephanie Weirich14 talks
- Alejandro Serrano Mena14 talks
- Nicolas Rinaudo13 talks
| title | conference | date |
|---|---|---|
| Imperative Syntax for Dependent Types | HATRA 2025 | 2025-10-14 |
Claim: an imperative surface syntax that elaborates into Idris makes dependently typed code more comprehensible for experienced imperative programmers. Built… | ||
| Type-level Property Based Testing | TyDe 2024 | 2024-09-06 |
An automated framework in Idris 2 runs type-level QuickCheck during compilation to test dependent-type models built as an indexed state monad. Properties… | ||
| Yaffle: A New Core for Idris 2 | WITS 2024 | 2024-01-20 |
Yaffle is a new core for Idris 2 implemented in Idris 2 itself, built to fix core bottlenecks and simplify checking. It compiles via Chez Scheme and bootstraps… | ||
| Quantitative Types in Idris 2 | SPLASH 2020 REBASE | 2020-11-16 |
A new Idris 2 core implements Quantitative Type Theory (Conor McBride, Bob Atkey) with concrete multiplicities 0 1 ω, enabling dependent+linear types. The… | ||
| Panel discussion: Types for All: From weak to strong, from static to dynamic | Code Mesh LDN 2020 | 2020-11-05 |
Panelists compare concrete systems and trade-offs: dependent types in Idris 2 (about 50,000 lines of Idris, with tests taking ~3x the build time) eliminate… | ||
| Dependent Type Driven Program Synthesis in Idris | Code Mesh LDN 2020 | 2020-11-05 |
Idris uses the type to synthesize program fragments by incremental case-splitting and expression search over holes and unification, generating batches (default… | ||
| Frex: indexing modulo equations with free extensions (Extended Abstract) | TyDe 2020 | 2020-08-23 |
An extensible Idris2 library implements equality-by-normalization for indices using free extensions, with a user tier (frexlets) and a developer tier (core… | ||
| Keynote – Edwin Brady | Scheme 2019 | 2019-08-18 |
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”… | ||
| Idris 2: Type-driven development of Idris | Code Mesh LDN 2018 | 2018-11-08 |
A new implementation rewrites the language in itself: Idris 2 implemented in Idris, with an interactive editor workflow (Atom protocol) that drives development… | ||
| Type-driven Development of Communicating Systems in Idris | Lambda World 2016 | 2016-09-30 |
Idris uses dependent types and totality checking to make concrete claims: total functions terminate or produce finite prefixes of infinite results, and IO is… | ||
| Type-Driven Development in Idris | Scala World 2015 | 2015-09-20 |
Idris provides first‑class dependent types and interactive tools (REPL, case‑split, expression search) that drive development: the language types compute… | ||
| Idris: Programming with Dependent Types | Code Mesh 2013 | 2013-12-03 |
Idris claims to bring full dependent types to practical programming with an optimising compiler and FFI, plus totality checker and tactic-based theorem… | ||
| Scala vs Idris: Dependent types, now and in the future | Strange Loop 2013 | 2013-09-18 |
A head-to-head of concrete engineering: Idris demonstrates full dependent types, builds sized vectors and an effects DSL that type-checks, compiles and runs… | ||
| nothing matches | ||