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 |
| Exam | 26 November 2026, 5.00 pm - 7.00 pm |
The Exam information shown may be subject to changes. Students are to check the finalised exam timetable with exam seat information, which will be available at the 'Examination Seating Arrangement' webpage, 2 weeks before start of examination.
Prerequisite Graph
Required first
MH1403Algorithms & ComputingMH1812Discrete MathematicsSC2001Algorithm Design & AnalysisSC2301Algorithm Design & AnalysisReasoning About Programs
Unlocks
Available Indexes
| Mon | Tue | Wed | Thu | Fri | |
|---|---|---|---|---|---|
| 930 | COMMON LEC (SCL4) 0930-1120 Mon LT8 | ||||
| 1000 | |||||
| 1030 | |||||
| 1100 | |||||
| 1130 | 10518 TUT (SCEL) 1130-1220 Mon LT8 Wk2-13 | ||||
| 1200 |
Other Relevant Mods
SC1001
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
Language & Logic