{"guid":"import-007ef07bf3c6b624be","title":"Certified programming with dependent types","subtitle":"Because the future of defense is liberal application of math","slug":"cccamp11-4426-certified_programming_with_dependent_types-en","link":"http://events.ccc.de/camp/2011/Fahrplan/events/4426.en.html","description":"Dependent types expand the concept of types in programming languages by arbitrary predicates depending on the value of the type. This lecture will introduce the concept and show how it can be used to develop formally verified code.\n","original_language":"eng","persons":["Andreas Bogk"],"view_count":271,"promoted":false,"date":"2011-08-12T02:00:00.000+02:00","release_date":"2011-08-14T02:00:00.000+02:00","updated_at":"2026-01-14T22:30:13.092+01:00","tags":["camp2011"," Science"],"length":5211,"duration":5211,"thumb_url":"https://static.media.ccc.de/media/conferences/camp2011/cccamp11-4426-certified_programming_with_dependent_types-en.jpg","poster_url":"https://static.media.ccc.de/media/conferences/camp2011/cccamp11-4426-certified_programming_with_dependent_types-en_preview.jpg","timeline_url":"https://static.media.ccc.de/media/conferences/camp2011/import-007ef07bf3c6b624be-timeline.jpg","thumbnails_url":"https://static.media.ccc.de/media/conferences/camp2011/import-007ef07bf3c6b624be-thumbnails.vtt","frontend_link":"https://media.ccc.de/v/cccamp11-4426-certified_programming_with_dependent_types-en","url":"https://api.media.ccc.de/public/events/import-007ef07bf3c6b624be","conference_title":"Chaos Communication Camp 2011","conference_url":"https://api.media.ccc.de/public/conferences/camp2011","related":[{"event_id":127,"event_guid":"import-d76d60d0cb3b8ff53f","weight":2},{"event_id":162,"event_guid":"import-c103a561a60405ea5c","weight":1},{"event_id":169,"event_guid":"import-3eee1d460ed0c3da7c","weight":2},{"event_id":176,"event_guid":"import-17f6892402aad51b39","weight":2},{"event_id":1496,"event_guid":"import-19a0b1ea628b75e61a","weight":1},{"event_id":1796,"event_guid":"z7M48Tb_4vtI0BBFVqe_ag","weight":1},{"event_id":1975,"event_guid":"1d9f168fd259ff3d","weight":1},{"event_id":1976,"event_guid":"b0167f2efcd6a228","weight":1},{"event_id":1987,"event_guid":"20EwnwJ17Oj0CmoP9_jZOA","weight":1},{"event_id":2367,"event_guid":"086bdbbf-0d17-437b-9ac8-bb7789da107c","weight":1},{"event_id":2735,"event_guid":"5c0323b6-c538-4fb6-8d70-d08def6bf865","weight":1},{"event_id":3033,"event_guid":"ea530d4e-c315-4fc4-86ef-f34f3a18f663","weight":1},{"event_id":3038,"event_guid":"cf873495-8beb-47f3-a303-4893400ecf30","weight":1},{"event_id":3813,"event_guid":"3161a4f1-ed69-49ae-b181-7ed1f6ad1d8d","weight":1},{"event_id":4259,"event_guid":"b5a645a9-bbdc-433e-a77c-b416074a92ea","weight":1},{"event_id":4589,"event_guid":"d13d0904-92a4-11e7-be40-5373c2f92fbe","weight":1},{"event_id":4861,"event_guid":"bdccda64-ee80-43fb-8e56-931199444188","weight":2}],"recordings":[{"size":440,"length":5211,"mime_type":"video/ogg","language":"eng","filename":"cccamp11-4426-certified_programming_with_dependent_types-en.ogv","state":"downloaded","folder":"video","high_quality":true,"width":720,"height":576,"updated_at":"2014-05-10T15:26:13.867+02:00","recording_url":"https://cdn.media.ccc.de/events/camp2011/video/cccamp11-4426-certified_programming_with_dependent_types-en.ogv","url":"https://api.media.ccc.de/public/recordings/180","event_url":"https://api.media.ccc.de/public/events/import-007ef07bf3c6b624be","conference_url":"https://api.media.ccc.de/public/conferences/camp2011"},{"size":440,"length":5211,"mime_type":"video/webm","language":"eng","filename":"cccamp11-4426-certified_programming_with_dependent_types-en.webm","state":"downloaded","folder":"video","high_quality":true,"width":720,"height":576,"updated_at":"2016-01-27T11:02:42.114+01:00","recording_url":"https://cdn.media.ccc.de/events/camp2011/video/cccamp11-4426-certified_programming_with_dependent_types-en.webm","url":"https://api.media.ccc.de/public/recordings/178","event_url":"https://api.media.ccc.de/public/events/import-007ef07bf3c6b624be","conference_url":"https://api.media.ccc.de/public/conferences/camp2011"},{"size":440,"length":5211,"mime_type":"video/mp4","language":"eng","filename":"cccamp11-4426-certified_programming_with_dependent_types-en.mp4","state":"downloaded","folder":"video","high_quality":true,"width":720,"height":576,"updated_at":"2016-01-27T11:02:42.079+01:00","recording_url":"https://cdn.media.ccc.de/events/camp2011/video/cccamp11-4426-certified_programming_with_dependent_types-en.mp4","url":"https://api.media.ccc.de/public/recordings/179","event_url":"https://api.media.ccc.de/public/events/import-007ef07bf3c6b624be","conference_url":"https://api.media.ccc.de/public/conferences/camp2011"}]}