u/edwardkmettin r/haskell • Recommends
Boston Haskell: Chris Casinghino - Making Dependent Types Practical
0:00 / 0:00
#dependenttypes#zombielanguage#typesystems
Chris Casinghino - Making Dependent Types Practical
Boston Haskell
1.1K subscribers • 18 videos on Hallway
- Recommended by 1 person: 1 in engineering communities.
- Presented by Chris Casinghino
Advanced. Deep dive for people who know the field.
3.5K views11 years ago1 recommendation
Programming languagesComputer scienceLanguage design and type systemsComputation and complexity
Chris Casinghino discusses the limitations of modern dependently typed languages and how the Zombie research language attempts to address them.
Aᴘʀɪʟ 15, 2015 @ Bᴏsᴛᴏɴ Hᴀsᴋᴇʟʟ: meetup.com/Boston-Haskell/events/219653486/ Sʟɪᴅᴇs: tyconmismatch.com/bh_talk.pdf "The last decade has seen many success stories for verified programming with dependent types, including the CompCert verified C compiler, verified libraries for concurrency and security, and machine-checked proofs of results like the four color theorem and the Feit-Thompson theorem. Despite these successes, dependently typed languages are rarely used for day-to-day programming tasks. In this talk, I’ll describe several limitations of modern dependently-typed languages that are holding them back from wider adoption for practical programming tasks. I’ll explain the historical and mathematical reasons for these limitations, and describe how we attempted to relax them in the design of the Zombie research language."