u/bjzabaPikelet, Fathomin r/ProgrammingLanguages • Recommends
CoqPL: Verifying a compiler through equational means
0:00 / 0:00
#coq#compilerverification#interactiontrees
[POPL 2021] CoqPL: Verifying a compiler through equational means
ACM SIGPLAN
11K subscribers • 53 videos on Hallway
- Recommended by 1 person: 1 in engineering communities.
- Presented by Yannick Zakowski, INRIA
Advanced. Deep dive for people who know the field.
992 views5 years ago1 recommendation
Systems programmingComputer scienceCompilers and interpretersFormal methods and verification
Yannick Zakowski presents a method for verifying compilers using equational reasoning and interaction trees in the Coq proof assistant.
Yannick Zakowski, INRIA popl21.sigplan.org/details/CoqPL-2021-papers/8/Verifying-a-c…