Hack-ing the Coq SSR

Olivier Danvy

(with suitable apologies to John Lennon, Paul McCartney, and Georges Gonthier)

Ooooh, got it from Inr'a web S.I.T.E.
Didn't get to bed last night
Oh the way the lecture notes were on my knee
Man I had a fruitful night
I'm hack-ing the Coq SSR
You do know how nerdy you are boy
Pack-ing the Coq SSR

Been at it so short I hardly know the pace
Gee Leibniz equa-lity
Blimey Howard Curry I construct my case
SS Reflect qua-lity
I'm pack-ing the Coq SSR
You do know how spunky you are boy
Hack-ing in Coq
Prov-ing in Coq
Us-ing the Coq SSR

Well the proof tactics really knock me out
They keep the rest behind,
And System F makes me sing and shout
Proof Gen'ral's always on my-my-my-my-my-my-my-my-my screen

Aw come on!
Ho yeah!
Ho yeah!
Ho ho yeah!
Yeah yeah!

Yeah I'm hack-ing the Coq SSR
You do know how plucky you are boy
Pack-ing the Coq SSR

Well the proof tactics really knock me out
They leave the rest unseen,
And System F makes me sing and shout
And Proof Gen'ral's always on my-my-my-my-my-my-my-my-my screen

IIII'll show you around my 'ductive the'rems way down screen
Make them dependently typed
Let me try this funky tactic matching out
Come and seek your QED
I'm hack-ing the Coq SSR
Hey you do know how cocky you are boy
Pack-ing the Coq SSR

Oh let me prove this lemma
Hey, the math!
I'm grooving with Coq SSR
Yes, Siree!
Yeah, hacking the Coq SSR

Ha ha

[Back to the course page]

Last modified: Thu Jan 3 18:33:21 +08 2019