Room 505, Cosmology Building, National Taiwan University + Cisco WebEx, Physical+Online Seminar
(實體+線上演講 台灣大學次震宇宙館505研討室+ Cisco WebEx)
Lean Where the Programming and Proof Meet
Hsin-Po Wang (National Taiwan University)
Abstract
With the latest development in AI, the resources Microsoft has put into Lean, and Tao and others' efforts in building the community, Lean will soon become as capable as a CS undergrad.
Lean can play two characters. It can be used as a usual programming language just like its predecessors Haskell and OCaml (the kind of languages taught at CS departments). It can also be used as a proof assistant, like Coq. Together, we can write programs and prove their properties in one go. In this seminar, we will demonstrate some examples of that and discuss its implications in industry and academia.
Organizer: Mao-Pei Tsui (NTU)
