These credits are primarily aimed at instilling basic notions which will be necessary not only for the formal methods and theoretical computer science thread but also to full understanding of various areas in computer science and general IT. These credits are compulsory to all IT students.

• Title: Mathematics of Discrete Structures
  Code: CSA 1060
  Credits: 4 ECTS
  Lectures: 24 hours
  Tutorials: 12 sessions in groups of 25-30 students
  Semesters: Held over semester 1 and 2
  Lecturer: Gordon Pace
  Examination: 30% exam in February, 70% exam in June. The resit will be in the form of one exam covering 100% of the final mark.
  

  Syllabus: The course is primarily aimed to introduce the basic mathematical tools that are required for the formal and rigorous treatment of the various aspects of computing. The importance of formal reasoning is emphasised in the course, concentrating on syntax, and formal proofs. The course also explains various mathematical notions and structures that will be used in later courses. The course introduces fundamental mathematical concepts - the use of axioms, rules of inference and syntactic definitions to express concepts in a precise mathematical notation, thus making them amenable to formal reasoning and proof.

  • Propositional Calculus: The use of truth tables, axiomatic and algebraic approaches, including the concept of soundness and completeness of formal models.
  • Predicate Calculus: Axiomatic approach to typed predicate calculus.
  • Typed Set Theory: A definitional approach based on predicate calculus allowing reasoning about sets.
  • Relations and Functions: Reasoning about relations and functions in terms of sets.
  • Natural Numbers and cardinality
  • Sequences, multisets, graph theory: These concepts are formalised in terms of the notions formalised earlier in the course.
  • Principle of Induction
  
  Textbooks and recommended reading list:
  • Gordon Pace, Mathematics of Discrete Structures, Lecture Notes, 2006.
  • Andrew Simpson, Discrete Mathematics by Example, McGraw-Hill, ISBN 0-07-709840-4, 2002.
  
  
  
• Title: Functional Programming (part of Declarative Programming)
  Code: CSA XXXX
  Credits: 3 ECTS (of 6 ECTS)
  Lectures: 14 hours
  Practicals: 10 sessions in groups of 25-30 students
  Semesters: Held in semester 2
  Lecturer: Joseph Cordina
  

  Examination: Assessment in a form of assignments contributing to 70% of the final mark and 30% in a written exam. Note that a pass in both assignments and the exam is required for a final pass. The resit will be in the form of a new assignment covering 70% of the mark and an oral exam covering 30% of the mark.

  Syllabus: This course gives an introduction to the functional programming paradigm, using Haskell. The course starts by explaining notions such as currying, strong typing, pattern matching, higher-order functions and advanced functional datatypes using practical examples. Evaluation order is discussed to explain the difference between call-by-value and call-by-name strategies, concentrating on lazy evaluation, the strategy used in Haskell. The practical part of the course finishes with an overview of type classes. This is then followed by a short overview of how we can prove properties of functional programs, from basic rewrite proofs to proofs requiring list and structural induction. The course will be complemented by a number of practical sessions in which you will discuss exercises that were handed out the week before.

  Aims of the Course Present Functional Programming as an alternative paradigm which fosters a mathematical reusable approach towards programming. Also to appreciate the benefits of a strongly type language.

  Topics Covered

  • Introduction: notation, currying, basic types, pattern matching, referential transparancy.
  • Lists and Tuples
  • Higher-Order Functions
  • Advanced Types: Enumerated types, parametrised types, data vs type.
  • Type Classes
  • Embedded Languages
  • Proving properties about functions
  • Evaluation Order and Lazyness
  Textbooks and recommended reading list:
  • Simon Thompson, The Craft of Functional Programming, Addison-Wesley, ISBN 0-201-34275-8, 1999. [Main textbook]
  • Richard Bird, Introduction to Functional Programming using Haskell, Prentice Hall Series in Computer Science, ISBN 0-13-484346-0, 1998.
  • Paul Hudak, The Haskell School of Expression: Learning Functional Programming through Multimedia, Cambridge University Press, ISBN 0-521-64408-9, 2000.

These credits are meant to build upon the students' basic understanding of computer science. They should be compulsory to students taking the computer science stream, and will be directly built upon by advanced formal methods and theoretical computer science credits.

• Title: Formal Languages and Automata (as part of Core Computer Science II)
  Code: CSA 2080 (Module 1)
  Credits: 3 ECTS
  Lectures: 21
  Tutorials: 4
  Semesters: Second semester
  Lecturer: Gordon Pace
  Examination: 30% assignments, 70% exam in June. The resit will be in the form of one exam covering 100% of the final mark.
  

  Syllabus: This module deals with the formal treatment of languages and automata (or machines) to recognise languages. The aims are not only at instilling the basic notions of languages, grammars and automata using formal mathematical notation but also provides a practical perspective, by applying the mathematical results to design parsers.

  The theory explored in the course will also be presented from a practical perspective, formalising automata and language recognisers using Haskell. The constructions used in the proofs covered in the course will also be expressed as programs, introducing the concept of provably correct algorithms.

  • Formal languages and grammars.
  • Regular languages: regular grammars, finite-state automata, regular expressions.
  • Context-free languages: context-free grammars, pushdown automata.
  • Closure properties of regular and context-free languages.
  • Normal forms for grammars.
  • Recognition algorithms for grammars.
  
  Textbooks and recommended reading list:
  • Gordon Pace, Formal Languages and Automata, Lecture Notes, 2003.
  • Peter Linz, An Introduction to Formal Languages and Automata (third edition), Jones and Barlett Publishers, ISBN 0-7637-1422-4, 2001.
  
  
• Title: Compiler Theory
  Code: CSI 2010
  Credits: 4 ECTS
  Lectures: 20
  Tutorials: 4
  Semesters: First semester
  Lecturer: Sandro Spina
  Examination: Assessment in a form of assignments contributing to 30% of the final mark and 70% in a written exam. Note that a pass in both assignments and the exam is required for a final pass.
  

  Syllabus: Compilers translate code from a source to a target language, the latter usually being a lower level language. The main aim of this course is to equip students with the necessary knowledge required to understand how modern compilers work. Moreover on a more practical note (as part of the assignment) students will be building a compiler for a small imperative programming language. The materials provided will be based on the Java programming language, however students can opt to work with other programming languages such as C or Haskell. The course will cover compilation both to JVM bytecode and native code. Apart from the usual topics associated with compiling theory the course will also offer introductions to the areas of compiler correctness and hardware compilers.

  Topics Covered (in no particular order)

  • grammars
  • lexers
  • parsers
  • abstract syntax
  • type systems (checking, derivations, type inference, etc)
  • syntax-directed translation
  • code generation and analysis (JVM, native)
  • register allocation
  • optimisation
  • compiler correctness
  • hardware compilers
  • Others that might be of interest to students
  
  Textbooks and recommended reading list:
  • Aho, Sethi, Ullman. /Compilers: Principles, Techniques, and Tools.
  • Andrew S. Appel, Modern Compiler Implementation in Java, Cambridge University Press, 1998. ISBN 0-521-60764-7
  
  
• Title: Advanced Functional Programming
  Code: CSI XXXX
  Credits: 2 ECTS
  Lectures: 14
  Tutorials: 10 sessions in groups of 25-30 students
  Semesters: Second semester
  Lecturer: Joseph Cordina
  

  Examination: Assessment in a form of assignments contributing to 70% of the final mark and 30% in a written exam. Note that a pass in both assignments and the exam is required for a final pass. The resit will be in the form of one oral exam covering 100% of the final mark.

  Syllabus: In this course more advanced topics of functional programming will be presented. It will be assumed that students have attended and completely successfully the first year Functional Programming course. The course will start with a quick recap of the important points in functional programming. Then the course will proceed to show advanced topics in functional programming that allow this paradigm to be useful in any problem domain. While introducing new topics, the students will be directed to the relevant literature on the subjects that might not be covered within the recommended text books. For each topic, efficiency improvements will be discussed together with advantages that a functional programming language gives over other programming paradigms. The last assignment will be chosen by the students themselves and discussed with the lecturer before writing the assignment.

  Topics Covered (in Alphabetical Order)

  • Concurrent Haskell
  • Equational Reasoning (structural induction)
  • Embedded of Languages and Examples
  • FFI
  • Graphics in Haskell
  • Lava as HDL
  • Monads
  • Monadic Parsers
  • QuickCheck
  • Others that might be of interest to students

  Aims of the Course Show Haskell as a viable programming language that can be applied to all problem domains. In addition, the students will appreciate the necessity of functional languages within industry today.

  Textbooks and recommended reading list:
  • Simon Thompson, The Craft of Functional Programming, Addison-Wesley, ISBN 0-201-34275-8, 1999.
  • Paul Hudak, The Haskell School of Expression: Learning Functional Programming through Multimedia, Cambridge University Press, ISBN 0-521-64408-9, 2000.
  • Jeremy Gibbons and Oege de Moor, Editors, The Fun of Programming, Palgrave Macmillan, ISBN 0-333-99-2857

These credits are aimed at advanced students who would like to further their knowledge in formal methods and theoretical computer science. Some of the credits will also be useful to support other computer science topic threads.

• Title: Computability and Complexity
  Code: CSA3100
  Credits: 2 ECTS
  Lectures: 14
  Semesters: First semester
  Lecturers: Gordon Pace
  Examination: 100% examination. The resit will also consist of an examination worth 100% of the mark.
  

  Syllabus: This course starts with an appraisal of Chomsky's language classes, aimed primarily at showing how different computation models (finite state automata, pushdown automata) have limits on what they can compute. This insight is extended to Turing Machines, leading to an overview of Church's Thesis, which states that all reasonable computation models are equivalent. The limits of computation are discussed, leading to the Halting Problem, and other non-computable functions. But not all computable functions are tractable. The course finishes with an overview of NP-completeness and an appreciation of the open problem of whether P=NP.

  • Chomsky's language hierarchy
  • Pumping lemmata to prove limits of each of Chomsky's language classes.
  • Turing Machines and the limits of computing.
  • Intractability, and NP-completeness
  
  Textbooks and recommended reading list:
  • Michael Sipser, Introduction to the Theory of Computation, PWS Publishing Company, ISBN 053494728X, 1997.
  • John E. Hopcroft, Rajeev Motwani, Jeffrey D. Ullman, Introduction to Automata Theory, Languages, and Computation (second edition), Addison-Wesley, ISBN 0201441241, 2001.
  
  
• Title: Formal Methods
  Code: CSA3230
  Credits: 4 ECTS
  Lectures: 24
  Semesters: First semester
  Lecturers: Gordon Pace, Sandro Spina, Joseph Cordina
  Examination: 100% assignment. The resit will consist of an assignment, in the form of a review of a number of papers assigned individually to the students.
  

  Syllabus: When designing safety-critical systems, it is not sufficient to test the software/hardware written, but it may be necessary to mathematically verify that the system works correctly. This course explores different topics in this research area, including mathematical tools (such as logics, and property languages), formal modelling of computer languages and systems, and techniques used for automatic model checking of such systems. The course covers different topics in theoretical computer science and formal methods which are not covered elsewhere in the degree, and may include:

  • Temporal logic
  • Process calculi
  • Synchronous programming
  • Formal semantics
  • Model checking of software and hardware

  Students will each present a different key-paper in the area of formal methods and will have to hand in a detailed review of their paper. They will also have to present a report on how 5 other papers presented by other students relate to their paper.

  The final mark is based on (i) class participation; (ii) delivery of a presentation on a chapter of the textbook and an assigned paper; and (iii) a final report on the topics covered in the course. Given that the course has no formal written examination, it is expected that the students participate fully throughout the whole course.

  Textbooks and recommended reading list:
  • E.M. Clarke, Orna Grumberg and Doron A. Peled, Model Checking, MIT Press, ISBN 0-262-03270-8, 1999.