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.
| AUs | 3.0 AUs |
| Grade Type | |
| Prerequisite | SC2001, SC2301, MH1403, MH1812 |
| 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 With | Yr1 |
| Not Available As BDE/UE To Programme | |
| Not Available As Core To Programme | |
| Not Available As PE To Programme | |
| Mutually Exclusive With | |
| Not Offered As BDE | |
| Not Offered As Unrestricted Elective | Yes |
| Exam |
Available Indexes
| Mon | Tue | Wed | Thu | Fri | |
|---|---|---|---|---|---|
| 930 | |||||
| 1000 | |||||
| 1030 | |||||
| 1100 | |||||
| 1130 | |||||
| 1200 | |||||
| 1230 | |||||
| 1300 | |||||
| 1330 | |||||
| 1400 | |||||
| 1430 | |||||
| 1500 | |||||
| 1530 | |||||
| 1600 | |||||
| 1630 | |||||
| 1700 | |||||
| 1730 | |||||
| 1800 |
Other Relevant Mods
SC1003
Introduction To Computational Thinking & Programming
SC1004
Linear Algebra For Computing
SC1005
Digital Logic
SC1006
Computer Organisation & Architecture
SC1007
Data Structures & Algorithms
SC1008
C & C++ Programming
SC1013
Physics For Computing
SC1123
Math 1: Linear Algebra & Calculus For Computing
SC1301
Writing Across The Disciplines