COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Trinity Mathematical Society > Dependent Type Theory - Proving Theorems by Writing Programs

## Dependent Type Theory - Proving Theorems by Writing ProgramsAdd to your list(s) Download to your calendar using vCal - Will Sonnex (Computer Lab)
- Sunday 04 March 2012, 14:00-14:30
- Winstanley Lecture Theatre, Trinity College.
If you have a question about this talk, please contact Mary Fortune. Part of the TMS Symposium A quick tutorial about writing programs in Agda, a language with dependently typed values. In Agda we can write a program, and then a mathematical proof that the program behaves correctly, in exactly the same language, through the magic of dependent types. This talk is part of the Trinity Mathematical Society series. ## This talk is included in these lists:Note that ex-directory lists are not shown. |
## Other listsneuroscience Cambridge Energy Conference Darwin Society## Other talksMicrosporidia: diverse, opportunistic and pervasive pathogens Lipschitz Global Optimization Hornby Model Railways Ancient DNA studies of early modern humans and late Neanderthals Beacon Salon # 8 The Dawn of the Antibiotic Age Prescribing step counts in type 2 diabetes and hypertension:Results of the Step Monitoring to improve ARTERial health trial |