2024 Faculty Courses School of Computing Department of Computer Science Graduate major in Computer Science
Mathematical Theory of Programs
- Academic unit or major
- Graduate major in Computer Science
- Instructor(s)
- Shin-Ya Nishizaki
- Class Format
- Lecture (HyFlex)
- Media-enhanced courses
- -
- Day of week/Period
(Classrooms) - 3-4 Mon / 3-4 Thu
- Class
- -
- Course Code
- CSC.T422
- Number of credits
- 200
- Course offered
- 2024
- Offered quarter
- 1Q
- Syllabus updated
- Mar 14, 2025
- Language
- English
Syllabus
Course overview and goals
Mathematical Theory of Programs is an area of theoretical computer science to build mathematical models of computer programs and to give a basis for analyzing, verifying and understanding their properties. In this course, you learn basic theories such as operational semantics, denotational semantics, axiomatic semantics and formal verification techniques for program behaviors. As applications of basic theories, you also learn domain theory.
Course description and aims
The main theme of this lecture is to build a basis to apply concept and theory of program theories such as operational semantics, denotational semantics, axiomatic semantics. Through this course, you learn the formal definitions of programming languages. You also learn techniques of proof for validations of program behavior in a level that you can apply them to another area of computer science through exercises.
Keywords
Operational Semantics, Denotational Semantics, Axiomatic semantics, Principles of induction, Hoare Logic, Domain theory, Concurrent Computation Model
Competencies
- Specialist skills
- Intercultural skills
- Communication skills
- Critical thinking skills
- Practical and/or problem-solving skills
Class flow
Classroom learning. After learning of basic concepts and definitions of formal semantics, study techniques of proof for validations of program behavior through running examples.
Course schedule/Objectives
| Course schedule | Objectives | |
|---|---|---|
| Class 1 | Formal semantics of programming languages | Understanding the importance of formal semantics of programming languages |
| Class 2 | Basic Concept | Explaining basic Concept of program theory |
| Class 3 | Operational Semantics (Expression valuation and Command execution) | Explaining operational Semantics (Expression valuation and Command execution) |
| Class 4 | Inductive definitions and principles of induction. | Explaining inductive definitions and principles of induction. |
| Class 5 | Proof rules for operational semantics | Explaining proof rules for operational semantics |
| Class 6 | Denotational Semantics | Explaining denotational semantics |
| Class 7 | The relationship between Operational Semantics and Denotational Semantics | Explaining the relationship between Operational Semantics and Denotational Semantics |
| Class 8 | Axiomatic semantics, Hoare Logic | Explaining axiomatic semantics, Hoare Logic |
| Class 9 | Soundness and Completeness of the Hoare rules | Explain soundness and completeness of the Hoare rules |
| Class 10 | Verification and Validation | Explaining verification and validation |
| Class 11 | Domain theory (1) Definitions | Explaining definitions in domain theory |
| Class 12 | Domain theory (2) Domain Theory and Various Properties | Explaining the domain theory and various properties |
| Class 13 | Models of Concurrent Computation: Definitions | Explaining the various definitions of concurrent models |
| Class 14 | Models of Concurrent Computations: Examples | Understanding of the model of concurrent computing through examples |
Study advice (preparation and review)
To enhance effective learning, students are encouraged to spend approximately 100 minutes preparing for class and another 100 minutes reviewing class content afterwards (including assignments) for each class.
They should do so by referring to textbooks and other course material.
Textbook(s)
None. Slides are available in lecture.
Reference books, course materials, etc.
Semantics with Applications: An Appetizer, Riis Nielson, Hanne, Nielson, Flemming ， Springer ， 2007
Communicating and mobile systems: the pi-calculus, Robin Milner, Cambrdge University Press.
Evaluation methods and criteria
The evaluation will be based on short reports (40%) and final exams (60%). However, the final exams may be replaced by a final report due to reasons such as the resurgence of COVID-19.
Related courses
- CSC.T261 ： Logic in Computer Science
- MCS.T416 ： Logic and Computation
Prerequisites
Mathematical Logic