Type Systems and Formal Hardware Verification.
主 题: Type Systems and Formal Hardware Verification.
报告人: 陈钢 博士 ((Boston University))
时 间: 0000-00-00
地 点: 理科一号楼1560
Explain what are type systems, the two applications of type systems:type for programming language and type system for proof assistant. Briefly introduce works on coercive subtyping in the Calculus of constructions. Finally, discuss on the possible application of using proof assistants for hardware verification.