POPL 2019 (series) / CoqPL 2019 (series) / The Fifth International Workshop on Coq for Programming Languages /
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.
Slides (coqpl2019_slides.pdf) | 2.40MiB |
Abstract (coqpl19-final8.pdf) | 521KiB |
Sat 19 Jan Times are displayed in time zone: Greenwich Mean Time : Belfast change
Sat 19 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change
16:00 - 17:40: Contributed Talks 4CoqPL at Sala VI Chair(s): Robbert KrebbersDelft University of Technology | |||
16:00 - 16:25 Talk | Deep Embedded Hoare Logic for Building Machine-Checkable Foundational Program Correctness Proofs CoqPL Qinxiang CaoShanghai Jiao Tong University File Attached | ||
16:25 - 16:50 Talk | Teaching Discrete Mathematics to Early Undergraduates with Software Foundations CoqPL File Attached | ||
16:50 - 17:15 Talk | Ltac2: Tactical Warfare CoqPL File Attached | ||
17:15 - 17:40 Talk | Towards a Coq Formalisation of Build Systems CoqPL File Attached |