The unit introduces the formal study of software systems. It is intended to provide a general basis for further study or research in softwarefocused areas of Computer Science such as Programming Languages and Formal Methods.
The unit is organised around two main themes:
a) The meaning of programs. To study software systems it is necessary to have a proper understanding of the programming languages in which those systems are written. Formal semantic descriptions of languages assign mathematical meanings to programs. Typical kinds of meaning that will be studied include types that specify the operations that programs will perform, and operational aspects that capture how a program behaves as it executes.
b) Techniques for verifying that languages and programs have desired properties. We will see how to analyse a language semantics to prove that all programs written in that language have desirable properties. E.g., a desirable property of a type system is type safety: that an executing program cannot execute an illegal operation. We will also study the properties of particular programs. E.g., it is often desirable to be able to prove that a program produces a desired result.
The practical work in the unit will include implementation of formal language semantics and development of verification proofs. We emphasise the use of frameworks and tools to assist with both of these activities. Examples include the use of software language engineering tools and libraries to assist with language implementation, and the use of proof assistants, program verification systems or model checkers to help us specify properties and to find proofs.
Students entering this unit should have reasonable programming experience and should have studied discrete mathematics. Relevant Macquarie University units for programming maturity are COMP225 Algorithms and Data Structures, COMP229 ObjectOriented Programming Practices and any 300level unit that applies programming skills to particular problem domains (e.g., COMP330 Computer Graphics, COMP333 Algorithm Theory and Design, and ISYS302 Advanced Application Development). DMTH137 Discrete Mathematics I and DMTH237 Discrete Mathematics II provide good mathematical background. Previous courses in areas such as programming language concepts or implementation, such as COMP332 Programming Languages, will be helpful, but are not required.
The class material will be structured according to the following schedule. The rightmost column refers to the relevant chapters of the "Software Foundations" required text. Note that there will be no class in Week 5 and Week 7 due to the Easter Monday and Anzac Day holidays, respectively.
Week 
Topic 
Chapter of Text 
1 
Introduction, Functional Programming 
Preface, Basics 
2 
Proof by Induction, Structured Data 
Induction, Lists 
3 
Polymorphism and HigherOrder Functions 
Poly 
4 
More basic tactics 
Tactics 
5 
Logical Reasoning 
Logic 
6 
Inductive Propositions 
IndProp 
78 
Maps, Imperative Programming Language 
Maps, Imp 
9 
Program Equivalence 
Equiv 
10 
Hoare Logic for Imperative Programs 
Hoare 
11 
Smallstep Operational Semantics 
Smallstep 
12 
SimplyTyped Lambda Calculus 
Stlc, StlcProp (overview) 
13 
Presentations, Review 
