This cour­se is an in­tro­duc­tion to in­ter­ac­tive theo­rem pro­ving and ad­van­ced func­tio­nal pro­gramming, most­ly using the Coq proof as­sis­tant.

This cour­se is for stu­dents in­te­rested in:

• The foun­da­tio­nal theo­ries of ma­the­ma­tics, most no­ta­b­ly type theo­ry and logic
• Prac­tical in­ter­ac­tive theo­rem pro­ving in a sta­te-of-the-art proof as­sis­tant
• Ad­van­ced func­tio­nal pro­gramming lan­gua­ges and their re­la­ti­on to con­struc­tive ma­the­ma­tics via the “Cur­ry-Howard Iso­mor­phism”
• Pro­gram ve­ri­fi­ca­ti­on and “cer­ti­fied pro­gramming”
• Pro­gramming Lan­gua­ge Se­man­ti­cs

Do­zen­ten

• Klaus Os­ter­mann
  HeadKlaus Os­ter­mann
• Ingo Sku­pin
  Alum­niIngo Sku­pin

Sche­du­le

Lec­tu­re: The lec­tu­re will take place on­line via Zoom on the fol­lo­wing dates:

• Tu­es­day, 10 c.t.
• Thurs­day, 10 c.t.

The Zoom room for this lec­tu­re is avail­able here: zoom lec­tu­re

Ex­er­cise group: The ex­er­ci­ses will take place on­line via Zoom on Fri­day, 12 c.t. The Zoom room for this ex­er­cise group is avail­able here: zoom ex­er­ci­ses

If you in­tend to par­ti­ci­pa­te in this lec­tu­re, plea­se re­gis­ter in the forum and fol­low the in­struc­tions in the “about” post of the ITP ca­te­go­ry.

• Alma entry: Alma

Lec­tu­res

Vi­de­os

Re­sour­ces

• The Coq Proof As­sis­tant Link
• The Soft­ware Foun­da­ti­ons Se­ries Link
• Adam Chli­p­a­la, Cer­ti­fied Pro­gramming with De­pen­dent Types CPDT