Event Location

Contact

For all queries in regards to this Event please contact the following :-

If you are having trouble making your payment for this conference, please contact:
Ms Soheni Datta (s.datta@ucl.ac.uk) 

If you require further details about the conference itself, please contact: 
Alex Walker (alexander.walker@ucl.ac.uk)

PLEASE ONLY CONTACT THE ONLINE STORE DIRECTLY IF YOU ARE EXPERIENCING PROBLEMS WITH YOUR DEBIT/CREDIT CARD PAYMENT, FOR ALL OTHER QUERIES RELATING TO THIS EVENT, INCLUDING CANCELLATIONS THESE SHOULD BE DIRECTED TO THE CONTACT DETAILS ABOVE.

More Information

Abstract :
An introduction to proofs course aims to teach how to write proofs informally in the language of set theory and classical logic. In this talk, I’ll explore the alternate possibility of learning instead to write proofs informally in the language of dependent type theory. I’ll argue that the intuitions suggested by this formal system are closer to the intuitions mathematicians have about their praxis. Furthermore, dependent type theory is the formal system used by many computer proof assistants both “under the hood” to verify the correctness of proofs and in the vernacular language with which they interact with the user. Thus, there is an opportunity to practice writing proofs in this formal system by interacting with computer proof assistants such as Rocq or Lean. Equally, intuitions built from an early informal introduction to dependent type theory will make it easier for those who aspire to write computer formalized proofs later on.