The Coq Proof Assistant, and Logical Foundations
You can find the Software Foundations class online at http://softwarefoundations.cis.upenn.edu. Coq and its IDE can be installed from https://coq.inria.fr/download.
Other Videos By Tea Leaves
2023-04-21 | ChipWits: The Interview |
2023-04-10 | Let's Play: Paper Mario The Thousand-Year Door |
2023-04-07 | Pascal Genie - Structured Program Editing in 1986 |
2023-04-01 | Teaching Haskell to Kids |
2023-02-19 | Talking To Andrew Plotkin about System's Twilight |
2023-02-18 | System's Twilight with Andrew Plotkin |
2023-02-13 | Can Programming Be Liberated From The Von Neumann Style? |
2023-02-12 | Can Programming Be Liberated From The Von Neumann Style? |
2023-01-15 | Taipan - a BASIC game, explored |
2022-12-29 | Removing Copy Protection With the Apple II Machine Language Monitor |
2022-12-03 | The Coq Proof Assistant, and Logical Foundations |
2022-11-19 | Process, Software, Twitter, and The Mythical Man-Month |
2022-10-29 | Santa Paravia: A 1978 Nation-Building Game |
2022-10-09 | An Elegant Solution for Personal Finance: Finances 2 |
2022-09-18 | Turing Complete, Part 8: XOR Frustration |
2022-09-10 | What's the Deal With I Bonds? Investing in a time of Inflation |
2022-09-03 | Plain Text Accounting: An Opinionated View |
2022-08-14 | Turing Complete, Part 7: Writing some Assembly Language! |
2022-08-05 | Turing Complete, Part 6: Computer, Completed |
2022-07-31 | Turing Complete Part 5: Conditionals |
2022-07-30 | Turing Complete, A NAND To Tetris game: Part 4 |
Tags: coq
proof assistants
software verification
formal verification
lean
agda
isabelle