CLASSES

Each week of COMP796 has three hours of face-to-face class. Classes will be a mixture of lecture-style presentation and hands-on practical work. 

REQUIRED AND RECOMMENDED TEXTS AND/OR MATERIALS

COMP796 will follow the book Software Foundations by Benjamin Pierce et al. (http://www.cis.upenn.edu/~bcpierce/sf/). The book is freely available from the web site and consists of annotated programs, proofs and exercises. It can be read in HTML form or the full distribution can be downloaded for formatting as PDF. This book is updated from time to time. We will use the most recent version which is dated 18 July 2013.

Students should read the relevant sections of the book and attempt the basic exercises on their own. Class time will be devoted to the main ideas of each chapter and working through a number of more advanced exercises. Some basic and more advanced exercises will be set as homework exercises.

UNIT WEBPAGE AND TECHNOLOGY USED AND REQUIRED

COMP796 Web Home Page: http://www.comp.mq.edu.au/units/comp796/

COMP796 uses iLearn for delivery of class materials, discussion boards, online selftests, submission of assessment tasks and access to marks and comments. Students should check the iLearn site regularly for unit updates.

Questions regarding the content of this unit, its tutorials or practicals should be posted to the appropriate discussion board on iLearn. In particular, any questions which are of interest to all students in this unit should be posted to one of these discussion boards, so that everyone can benefit from the answers.

Coq Proof Assistant 

The practical work in this unit involves functional programming and proof construction using the Coq proof assistant (http://coq.inria.fr). Ideally, students should install Coq on a laptop and bring it to class so they can follow along with in-class exercises.

WHAT HAS CHANGED?

This unit is "Advanced Topics in Theory and Practice of Software". 

The unit introduces the formal study of software systems. It is intended to provide a general basis for further study or research in software-focused 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 Object-Oriented Programming Practices and any 300-level unit that applies programming skills to particular problem domains (e.g., COMP330 Computer Graphics, COMP333 Algorithm Theory and Design, and ISYS302 Advanced Application Development). DMTH237 Discrete Mathematics II is good background in that area. 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. 

COMP796 will be assessed and graded according to the University assessment and grading policies.

Submission Deadlines

Assessment deadlines are strict, unless an application for special consideration is received (preferably in advance) accompanied by appropriate documentary evidence. Late submissions will be penalised at the rate of 20% of the full marks for the assessment per day or part thereof late.

Standards

The following general standards of achievement will be used to assess each of the assessment tasks with respect to the letter grades. 

Pass: Has a basic undestanding of language and program semantics as discussed in class. Can use a verification tool or proof system to specify and prove simple language and program properties similar to those discussed in class. Can perform a basic research investigation in the area and present the results of that research in rudimentary written and oral forms.

Credit: As for Pass plus: Is able to apply the techniques we have discussed to specify and prove new properties that are not direct analogues of ones discussed in class. Shows more than basic insights into the results of a research investgiation and is able to communicate those insights.

Distinction/High Distinction: As for Credit plus: Is able to generalise from the language and program properties discussed explicity to new ones for problem domains not explicitly discussed in class and can apply verification tools and systems to proofs about them. Can critically evaluate the limits of the techniques and tools we have discussed.

Assessment Process

These assessment standards will be used to give a numeric mark out of 100 to each assessment submission during marking. The mark will correspond to a letter grade for that task according to the University guidelines. The final raw mark for the unit will be calculated by combining the marks for all assessment tasks according to the percentage weightings shown in the assessment summary.

We will look at your overall performance on all assessments when determining your final grade. A total raw mark of at least 50% and a mark of at least 50% on each of the four assessment categories will be sufficient to pass the unit. Students who do not meet this cut-off will be examined on a case-by-case basis.

On occasion your raw mark for the unit may not be the same as the Standardised Numeric Grade (SNG) which you receive as the result. Under the Senate guidelines, raw marks may be scaled to ensure that there is a degree of comparability across the university, so that units with the same past performances of their students should achieve similar results.