As a computational model of functional programming languages, the lambda calculus is introduced in the class, mainly focused
in its syntactic part. Besides, a mechanism to evaluate lambda terms called SECD machine, and another computational model
for functional programming languages called combinatory logic are also described.

Understaiding a computational model for functional programming langhuages by learning and understaiding the theory of lambda
calculus.

- Understanding theoretical aspects of programming languages.
- Understanding a mathematical theory Lambda Calculus for modeling programming languages.
- Understanding ways of thinking programs mathematically.

Class schedule | HW assignments (Including preparation and review of the class.) | Amount of Time Required | |
---|---|---|---|

1． | Models of Programmina Languages (1): Necessity of Computational Models | Understanding the contents of the class. | 120minutes |

2． | Models of Programmina Languages (2): Lambda terms and some notions | Understanding the contents of the class. | 200minutes |

3． | Models of Programmina Languages (3): Beta reduction | Understanding the contents of the class. | 200minutes |

4． | Models of Programmina Languages (4): Confluency of Reduction | Understanding the contents of the class. | 120minutes |

5． | Models of Programmina Languages (5): Models of Programming Languages based on the Lambda Calculus | Understanding the contents of the class. | 200minutes |

6． | Typed Lambda Calculus (1): Constants and Base Types, Definition of Typed Lambda Terms | Understanding the contents of the class. | 210minutes |

7． | Typed Lambda Calculus (2): Simple Typed Lambda Calculus and Its Definition | Understanding the contents of the class. | 210minutes |

8． | Typed Lambda Calculus (3): de Brujin index and bound variables | Understanding the contents of the class. | 210minutes |

9． | Typed Lambda Calculus (4): Denotational Semantics of the Simple Typed Lambda Calculus, Set Theoretic Model | Understanding the contents of the class. | 210minutes |

10． | Typed Lambda Calculus (5): Denotational Semantics of the Simple Typed Lambda Calculus, Domain Theoretic Model | Understanding the contents of the class. | 210minutes |

11． | Typed Lambda Calculus (6): Axiomatic Semantics of the Simple Typed Lambda Calculus | Understanding the contents of the class. | 210minutes |

12． | Typed Lambda Calculus (7): What is Soundness and Completeness of the Axiomatic Semantics | Understanding the contents of the class. | 210minutes |

13． | Typed Lambda Calculus (8): Soundness of the Axiomatic Semantics | Understanding the contents of the class. | 210minutes |

14． | Typed Lambda Calculus (9): Completeness of the Axiomatic Semantics | Understanding the contents of the class. | 210minutes |

Total. | - | - | 2730minutes |

Report | Total. | |
---|---|---|

1. | 40% | 40% |

2. | 40% | 40% |

3. | 20% | 20% |

Total. | 100% | - |

Based on reports.

Students who can calculate beta-reductions, and understanding the basics of the lambda calculus will be graded as 60%.

Students who can calculate beta-reductions, and understanding the basics of the lambda calculus will be graded as 60%.

[Reference]

- H. P. Barendregt, "The Lambda Calculus - Its Syntex and Semantics", Studies in Logic and the Foundations of Mathematics, vol.103, Elsevier.

- H. P. Barendregt, "The Lambda Calculus - Its Syntex and Semantics", Studies in Logic and the Foundations of Mathematics, vol.103, Elsevier.

Students must have experiences on programmin, and familiar with mathematical concepts like sets, functions.

- Non-social and professional independence development course

Work experience | Work experience and relevance to the course content if applicable |
---|---|

N/A | N/A |

Last modified : Sun Mar 21 17:18:11 JST 2021