This course will introduce you to the mathematical foundations behind programming languages and the principles of rigorous program reasoning. Students will become confident computational thinkers with an appreciation for how software design can be guided by contract-based reasoning and how modern software implementations can be safeguarded by language features such as type systemsand principled program analysis.These techniques are the basis for several professional activities in computer science:- Designing, specifying, and standardising programming languages (e.g. ISO [C/C++], ECMA [JS], W3C [Wasm])- Developing program analysis and bug-finding tools (e.g. Typescript, Facebook's Infer)- Conducting formal verification of safety-critical systems (e.g. CompCert). This course also serves as a gateway to more advanced research topics in computer science, such as type theory, separation logic, and mechanised theorem proving.
| Academic Units | 3 |
| Exam Schedule | Not Applicable |
| Grade Type | Letter Graded |
| Department Maintaining | CSC(CE) |
| Prerequisites | |
| Not Available to Programme | ACBS, ACC, ADM, AERO, AISC, ARED, ASEC, BACF, BASA, BEEC, BIE, BMS, BS, BSB, BSPY, BUS, CBE, CBEC, CEE, CHEM, CHIN, CMED, CNEL, CNLM, COMP, CS, CVEC, ECMA, ECON, ECPP, ECPS, EEE, EEEC, EESS, ELAH, ELH, ELHS, ELPL, ENE, ENEC, ENG, ESPP, HIST, HSCN, HSLM, IEEC, IEM, LMEL, LMPL, LMS, MAT, ME(DES), ME(IMS), ME(NULL), ME(RMS), MEEC(DES), MEEC(IMS), MEEC(NULL), MEEC(RMS), MS, MS-2ndMaj/Spec(MSB), MTEC, PESC, PHIL, PHMS, PHY, PLCN, PLHS, PPGA, PSLM, PSMA, PSY, REP(ASEN), REP(BIE), REP(CBE), REP(CVEN), REP(EEE), REP(ENE), REP(MAT), REP(ME), ROBO, SCED, SOC, SPPE, SSM |
| Not Available to All Programme | Yr1 |
| Index | Type | Group | Day | Time | Venue | Remark |
|---|
0930
1030
1130
1230
1330
1430
1530
1630
1730
We would encourage you to review with the following template.
AY Taken: ...
Assessment (Optional): ...
Topics (Optional): ...
Lecturer (Optional): ...
TA (Optional): ...
Review: ...
Final Grade (Optional): ...