Skip to main content

All Questions

Tagged with
Filter by
Sorted by
Tagged with
2 votes
1 answer
124 views

What are the differences between LCF's Theorem and Automath's Prop?

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 ...
user3565552's user avatar