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: Belfast change
16:00 - 17:40
|Deep Embedded Hoare Logic for Building Machine-Checkable Foundational Program Correctness Proofs|
Qinxiang CaoShanghai Jiao Tong UniversityFile Attached
|Teaching Discrete Mathematics to Early Undergraduates with Software Foundations|
|Ltac2: Tactical Warfare|
|Towards a Coq Formalisation of Build Systems|