11

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 in these systems (though usually not silently, as Andrej suggests), and the fix to that bug involves some changes to existing proofs, or, more likely, of the ...


4

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$. $\alpha$-equivalence and capture-avoiding substitution is an important concept to understand in type theory: I would recommend studying this concept for the ...


1

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)sound for a given term, in the sense that the underlyung type system would be (un)sound if it allowed assigning this type. Nowadays, type soundness is typically ...


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