Instructor | Yuxin Deng |
---|---|

Office | Room B1115, Science Building |

Office Hour | 10am - 2pm, Monday - Friday |

Phone | 021-62231281 |

yxdeng(AT)sei.ecnu.edu.cn | |

Homepage | basics.sjtu.edu.cn/~yuxin/ |

- Glynn Winskel. The Formal Semantics of Programming Languages: An Introduction. The MIT Press, 1993.
- John C. Mitchell. Foundations for Programming Languages. The MIT Press, 1996.
- Robert Harper. Practical Foundations for Programming Languages.
- Benjamin C. Pierce et al. Software Foundations.
- Peter Selinger. Lecture Notes on the Lambda Calculus.

- Basic set theory
- Introduction to operational semantics
- Some principles of induction
- Inductive definitions
- Denotational semantics
- Axiomatic semantics
- Completeness of the Hoare rules
- The untyped lambda calculus
- Introduction to domain theory
- Recursion equations
- Techniques for recursion
- The simply typed lambda calculus
- Languages with higher types
- Recursive types
- Theorem proving with Coq

- Attendance records: 10%
- Final written exam: 90%

Back