Why Type Theory matters

Note: Proposition (命题, 主张) means Claim / Fact

Proposition as Types vs (Classical) Propositional Logic vs Predicate Logic

With “Proposition as Types“, we can prove theorems using computers.

\boxed {\frac {\text {Proofs} }{\text {Propositions}} =\frac {\text {Programs}}{\text {Types}} }

… Propositions written in “Type” forms (right column).

Prove Tautology :

Prove: “To be” or “Not To be” (Shakespeare’s 《Hamlet》)

Naive Type Theory

Thorsten Altenkirch -| Lambda Days 2019

“Why Type Theory Matters ? “

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s