Dependent Type Driven Program Synthesis in Idris | Edwin Brady | Code Mesh V 2020

Edwin Brady demonstrates how Idris uses dependent types to interactively synthesize program fragments from type specifications.

This video was recorded at Code Mesh V 2020 - codesync.global/conferences/code-mesh-ldn/ Dependent Type Driven Program Synthesis in Idris | Edwin Brady - Lecturer in Computer Science at the University of St Andrews in Scotland ABSTRACT Idris is a functional programming language with first-class types, where types may be parameterised by other values. This allows us to give increasingly precise specifications for functions, and be more confident in their correctness. But, perhaps more importantly, it gives the language implementation more information up front about what a function should do. Therefore, we can use Idris as an interactive assistant, and treat programming as a conversation with the machine. In particular, the Idris system supports program synthesis, generating (fragments of) programs from types. In this talk, I will show the current state of program synthesis in Idris, outline how it works, and discuss some possible future research directions. • Follow us on social: Website: codesync.global/conferences/code-mesh-ldn/ Twitter: twitter.com/CodeMeshIO • Looking for a unique learning experience? Attend the next Code Sync conference near you! See what's coming up at: codesync.global • SUBSCRIBE TO OUR CHANNEL youtube.com/channel/UC47eUBNO8KBH_V8AfowOWOw