11 votes

Has a proof checker bug ever invalidated a major proof?

To my knowledge, no machine checked proof of a complex mathematical development has ever been retracted. As Andrej points out though, it occasionally happens that soundness-breaking bugs do crop up ...
  • 13.3k
4 votes

Pi-calculus (or session types) - proof for weakening lemma

You should $\alpha$-rename to avoid conflict with the variable names. That is, you should prove weakening of the form: $\Gamma \vdash (\upsilon y) P$ implies $\Gamma, x : T \vdash (\upsilon y) P$. $\...
  • 196
1 vote

Soundness of type (systems)

The standard text book would be Benjamin Pierce, "Types and Programming Languages". Technically, soundness is a property of a type system. Sometimes we also say informally that a type would be (un)...

Only top scored, non community-wiki answers of a minimum length are eligible