type theory and well-founded sets
Program Verification
Proving certain properties about programs—perhaps types, but not just types.
Program verification proofs are usually written manually, but uses a proof assistant which…
proof assistant
Helps with proof, by:
- checking the proof for correctness (uses type theory)
- helps automate the easy parts