Completed
Deep Specifications
Class Central Classrooms beta
YouTube videos curated by Class Central.
Classroom Contents
Verifying the LLVM
Automatically move to the next video in the Classroom when playback concludes
- 1 Intro
- 2 Collaborators
- 3 PLAN • LLVM Intermediate Representation
- 4 LLVM Compiler Infrastructure
- 5 Other LLVM IR Features
- 6 But... it's complex
- 7 One Example: undef
- 8 Interactions with Optimizations
- 9 What's the problem?
- 10 Compiler Bugs
- 11 Deep Specifications
- 12 Inspiration: CompCert
- 13 The Vellvm Project
- 14 Vellvm Framework
- 15 LLVM IR Semantics
- 16 Writing Interpreters in Coq
- 17 Interaction Trees
- 18 LLVM Interpreter in Cog
- 19 mem2reg register promotion
- 20 Caveats
- 21 Getting started with Cog
