~/talk

Verified Programming of Turing Machines in Coq

on YouTube 22m
Talkat CPP 2020 · 2020-01-20..01-21· [compilers-and-language-design]

speaker

name:Fabian Kunze
links:none on file

resources

video:https://youtu.be/HKrIMvC4xTA
slides:none on file

summary

Formal development in Coq of Turing machines and their programming, including definitions of machines, encodings, and correctness proofs. Uses Coq to verify that implemented Turing machine programs satisfy their specifications and to reason about computability and reductions within the Coq proof assistant.

AI-written summary · about

chapters (6)

  1. 0:00Verified Turing Machines in Coq
  2. 3:21Verification core concepts
  3. 8:08Case studies and apps
  4. 13:16Encoding overhead
  5. 16:13Future directions
  6. 20:51Conclusion & Q&A

related talks

~/search
type to search 6,249 conferences, 138,987 speakers and 185,172 talks
~/help
cmdctrl k
search every conference, speaker and series
/
focus the filter search
h
home
c
conferences
s
speakers
e
series
t
light / dark — the status bar button does the same
?
this help
esc
close this, then clear every filter — or just the search, while you are typing in it

Ignored while you are typing. Pages without a filter rail have no search to focus.