Dominic Orchard - Quantitative program reasoning in Granule via graded modal types | Code Mesh LDN
This video was recorded at Code Mesh LDN 19 - http://bit.ly/37xc3Nr Get involved in Code Sync's next conference - http://bit.ly/2Mcm4aS --- QUANTITATIVE PROGRAM REASONING IN GRANULE VIA GRADED MODAL TYPES by Dominic Orchard THIS TALK IN THREE WORDS: Types for Verification TALK LEVEL: Intermediate ABSTRACT A benefit of static typing is that various program properties can be specified and automatically checked as part of a language. But there are always limits to what can be expressed. This talk presents Granule, a functional language which pushes these limits by combining linear and indexed types with the recent notion of graded modal types. We'll see examples enforcing privacy constraints, stateful protocols, and verifying properties of standard functional programs just by getting the right type signature. Slides & full abstract: https://codesync.global/speaker/dominic-orchard/ --- THE SPEAKER - DOMINIC ORCHARD Computer science lecturer and co-creator of the Granule language Dominic is a computer science researcher and lecturer, interested in mathematically structured programming and lots else, at the School of Computing, University of Kent More on Dominic Orchard: https://codesync.global/speaker/dominic-orchard/ --- CODE SYNC & CODE MESH LDN 19 Code Mesh LDN is powered by Code Sync. Code Mesh LDN 19 was sponsored by WhatsApp, Microsoft, Erlang Solutions, Juxt, aeternity, Duffel, and IOHK. CODE SYNC Website: www.codesync.global Twitter: www.twitter.com/CodeMeshIO Facebook: https://www.facebook.com/CodeSyncGlobal LinkedIn: https://www.linkedin.com/company/code-sync/ Mail: info at codesync.global #Granule #FunctionalProgramming