Teaching Discrete Mathematics to Early Undergraduates with Software Foundations
We will present our early experiences teaching first- and second-year computer science students in Coq, adapting Logical Foundations (the first volume of Software Foundations). Our presentation’s goals are: to offer evidence that such a course is pedagogically sound; to highlight the pedagogical approach taken to teaching Coq and informal proof simultaneously; to document successes and failures, both pedagogically and in Coq’s technical ecosystem; and to seek feedback on pedagogy and course design.
The first author will give the talk.
Sat 19 Jan Times are displayed in time zone: Greenwich Mean Time : Belfast change
|16:00 - 16:25|
|Deep Embedded Hoare Logic for Building Machine-Checkable Foundational Program Correctness Proofs|
Qinxiang CaoShanghai Jiao Tong UniversityFile Attached
|16:25 - 16:50|
|Teaching Discrete Mathematics to Early Undergraduates with Software Foundations|
|16:50 - 17:15|
|Ltac2: Tactical Warfare|
|17:15 - 17:40|
|Towards a Coq Formalisation of Build Systems|