Experimenting a proof-assistant design based on refinement types: let's prove stuff

Channel:
Arnaud Spiwack
Subscribers:
29
Published on ● Video Link: https://www.youtube.com/watch?v=gKXy0R7nxbU


Duration: 3:21:26
0 views
0

Some of the audio, in the Twitch video, is muted because of copyright claims (probably abusive, as the music I used for this episode is supposed to be public domain recordings). The export, fortunately, is not muted. However, similar copyright claims occurred on Youtube. One of the segment I had to ask Youtube to remove the music. It's much better than muting my voice altogether, but it will not be perfect, so sound may sound weird, while I discuss how much I love the Rhapsody in Blue, which, unfortunately you won't be able to hear.

The code is hosted on github at https://github.com/aspiwack/peppermint-prover/.


Original video at https://www.twitch.tv/videos/716068695



 -- Watch live at https://www.twitch.tv/notnotarnaud



Other Videos By Arnaud Spiwack


2021-02-20Randomizer engine | Generalising to datalog: Relational Algebra to SAT | FP | Ocaml
2021-02-14Returning to the randomizer engine | Generalising to datalog | FP | Ocaml
2020-12-10Experimenting a proof-assistant: let's play with lsp and and repay some technical debt |FP | Haskell
2020-12-10Experimenting a proof-assistant design based on refinement types: a lispy syntax for tactics
2020-11-11Proof assistant detour: let's write a supercompiler (part 3) | FP | Haskell
2020-09-29Experimenting a proof-assistant design based on refinement types: let's try to do quotient types
2020-09-29Experimenting a proof-assistant design based on refinement types: where I get side-tracked a little
2020-09-29Experimenting a proof-assistant design based on refinement types: refactoring the syntax
2020-09-29Experimenting a proof-assistant design based on refinement types: refactoring session
2020-09-29Experimenting a proof-assistant design […]: propositions as terms, for real this time
2020-09-29Experimenting a proof-assistant design based on refinement types: let's prove stuff
2020-09-29Proof assistant detour: let's write a supercompiler
2020-09-29Proof assistant detour: let's write a supercompiler (part 2)
2020-09-29Where I attempt to fix a Keyboard.io Model 01 on stream
2020-05-20Experimenting a proof-assistant design based on refinement types: shadowing & type-checking tactics
2020-05-20Experimenting a proof-assistant design based on refinement types: tackling implication with focusing
2020-04-26Experimenting a proof-assistant design based on refinement types: more proofs & tactics | FP | Haske
2020-04-26Experimenting a proof-assistant design based on refinement types: adding interactivity | FP | Haskel
2020-04-25Experimenting a proof-assistant design based on refinement types | FP | Haskell
2020-04-25Experimenting a proof-assistant design based on refinement types: basic proofs | FP | Haskell
2019-09-07How does compression work? (Livecoding in Haskell)


Tags:
twitch
programming
mathematics
proof assistant
refinement types
dependent type
functional programming
haskell