How are the fundamental approaches to proving theorems by LCF and Automath different? Considering their modern descendants - Isabelle for LCF and Coq for Automath, both rely on type checking to do proof checking.
Theorems in Isabelle have a
theorem type and the only functions that can create instances of this
theorem type are inference rules of the logic.
Theorems in Coq have a
Prop type and the only way to create
Props is by creating proof terms that have the proposition as their types.
If I'm not wrong, LCF and Automath were developed independently around the same time so there wasn't an influence from one to the other, but perhaps by coincidence, is LCF's (Isabelle's)
Theorem just a more generic version of Automath's (Coq's)
I would appreciate it if you could also point out any other fundamental differences between LCF and Automath that have manifested into their modern successors.