本次逻辑前沿讨论班我们请到上海交大的曹钦翔作关于集合论形式化的报告。曹钦翔教授是我们哲学系2013届系友, 而今年正值我们哲学系110周年和逻辑学教研室成立70周年, 之后我们也将有更多的系友报告. 

标题（由于微信公众号标题字数限制，下面才是正式的标题）

Yet Another ZFC Set Theory Formalization in a Theorem Prover

时间

2022.9.6, 15:10-18:00

腾讯会议号: 657-824-601

链接可点击原文获得

摘要

Theorem provers can check formalized definitions and proofs. Typical theorem provers like Coq, Isabelle etc. has been widely used for building up huge proofs --- topics range from logics, analysis to program semantics. But for now, users of theorem provers are mainly professionals, researchers and well-trained Ph.D students. It usually takes weeks learning to use a theorem prover. In this talk, I will introduce a new formalization of ZFC set theory in Coq. I have used it in teaching first order logic proof rules and ZFC set theory. It is designed in a way that students can easily learn how to use it, build simple formalized proof by themselves and practice directly what they have learned in class.

报告人简介

本科毕业于北京大学，博士毕业于美国普林斯顿大学，2018年回国任教，现为上海交通大学约翰霍普克洛夫特计算机科学中心副教授、博导，2019年入选上海市浦江人才计划。曹钦翔长期从事基于交互式定理证明的程序验证工具开发，并研究有关程序逻辑特别是分离逻辑的理论问题。曹钦翔是Verified Software Toolchain（VST）工具的主要开发者之一，该工具首次实现了从业务逻辑，到源代码开发，再到编译的全链条正确性验证。