Reasoning About Programs

Current offering — AY2026/2027 Semester 1

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.

Total hours per week: 3 hrs

AUs	3.0 AUs
Grade Type
Prerequisite	SC2001, SC2301, MH1403, MH1812
Exam

Prerequisite Graph

Required first

MH1403Algorithms & Computing MH1812Discrete Mathematics SC2001Algorithm Design & Analysis SC2301Algorithm Design & Analysis

SC3270

Reasoning About Programs

Unlocks

No modules unlocked

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 offerings

AY25/26

Semester 1Semester 2Sp. Term

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

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

Mon

Tue

Wed

Thu

Fri

930

1000

1030

1100

1130

1200

1230

1300

1330

1400

1430

1500

1530

1600

1630

1700

1730

1800

Not Available To Programme	ACBS, ACC, ADM, ADMC, AERO, AISC, ARED, ASEC, BACF, BASA, BEEC, BIE, BMS, BS, BSB, BSPY, BUS, BUSD, BUSS, 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(IDMS), ME(IMS), ME(NULL), ME(RMS), MEEC(DES), MEEC(IDMS), 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

Not Available To Programme	ACBS, ACC, ADM, ADMC, AERO, AISC, ARED, ASEC, BACF, BASA, BEEC, BIE, BMS, BS, BSB, BSPY, BUS, BUSD, BUSS, 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(IDMS), ME(IMS), ME(NULL), ME(RMS), MEEC(DES), MEEC(IDMS), 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

	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	10518 TUT (SCEL) 1130-1220 Mon LT8 Wk2-13