名古屋大学 大学院多元数理科学研究科・理学部数理学科
住所: 〒464-8602 愛知県名古屋市千種区不老町

教育・就職 - 2023年度 - 卒業研究シラバス - J. ガリグ

  • WELCOME
  • 行事予定
  • 交通案内
  • 進学案内
  • 教育・就職
  • 研究情報
  • 人々
  • ジャーナル
  • 名古屋大学 理学図書室
  • 採用情報
  • 社会連携
  • 名古屋大学数理科学同窓会
  • アーカイブ
  • リンク

ファイル更新日:2022年11月25日

教育・就職

卒業研究シラバス


J. ガリグ

学部・大学院区分
Undergraduate / Graduate
理学部
時間割コード
Registration Code
科目区分
Course Category
専門科目
科目名【日本語】
Course Title
数学研究
科目名【英語】
Course Title
Undergraduate Seminar
コースナンバリングコード
Course Numbering Code
担当教員【日本語】
Instructor
GARRIGUE JACQUES
担当教員【英語】
Instructor
GARRIGUE JACQUES
単位数
Credit
6
開講期・開講時間帯
Term / Day / Period
春 水曜日 3時限
春 水曜日 4時限
授業形態
Course style
セミナー
学科・専攻
Department / Program
数理学科
必修・選択
Compulsory / Selected
選択必修
授業の目的【日本語】
Goals of the Course(JPN)
テーマ: プログラミング言語と型

プログラミング言語は正確に定義されなければならない.構文的な規則と意味的な規則によってその挙動が細かく規定される.前者は形式言語理論,後者は型理論や意味論という計算機科学特有の分野に発展している.
この卒業研究ではプログラミング言語を理解するための基礎理論を見て行く.
プログラミング言語の基礎概念を学び,型システムや意味論の形式化や証明を理解することを目標とする.また,聴衆を前にして数学的に筋道の通った話ができ,質問に対して的確に受け答えできるようになることも卒業研究の重要な目標になる.
授業の目的【英語】
Goals of the Course
Theme: Programming languages and type systems

A programming language should have a precise definition. Its behavior can be defined through grammatical and semantical rules. The former come from formal language theory, the latter from type theory and formal semantics, all independent areas of theoretical computer science.

In this undergraduate seminar we study the formal theory required to understand formally programming languages.

The goal of this seminar is to learn the fundamental concepts of programming languages, and understand the formal aspects and proof techniques of types systems and semantics. Being able to present a mathematically coherent account of the subject, and handle questions, is another important goal.
到達目標【日本語】
Objectives of the Course(JPN)
型システムの定義の仕方と基本性質(健全性など)の証明方法の理解.
様々な意味論の存在とその使い方の理解.
到達目標【英語】
Objectives of the Course
One shall acquire how a type is defined, and how to prove basic properties such as type soundness.
Understanding various semantics and their applications.
授業の内容や構成
Course Content / Plan
前期はプログラミング言語を定義する方法を見る.そこでは,有限オートマトン,文法,型システムや意味論が使われる.
後期は型システムや意味論をさらに深く調べる.
実施方法として,週に1回,おもに輪講形式のセミナーによって,文献を読み進めていく.
履修条件
Course Prerequisites
定員超過の場合の選考方法: オフィスアワーやビデオ通話などで面談した学生を優先する.
This seminar is expected to be conducted in Japanese
関連する科目
Related Courses
数理解析・計算機数学II (後期)
成績評価の方法と基準
Course Evaluation Method and Criteria
発表やレポートに基づいて評価
不可(F)と欠席(W)の基準
Criteria for “Fail(F)” & “Absent(W)” grades
履修取り下げによる
教科書・テキスト
Textbook
* 大堀・ガリグ・西村「コンピュータサイエンス入門 アルゴリズムとプログラミング言語」(岩波書店)1999年
五十嵐淳「プログラミング言語の基礎概念」(サイエンス社) 2011年
* Benjamin C. Pierce「型システム入門 プログラミング言語と型の理論」(オーム社)2013年
参考書
Reference Book
上記のうち,輪講に使われなかったもの,および講義中に適宜紹介したもの
課外学習等 (授業時間外学習の指示)
Study Load(Self-directed Learning Outside Course Hours)
特になし
注意事項
Notice for Students
なし
質問への対応方法
How to Ask Questions
対面以外にはメールなどもか
他学科聴講の可否
Propriety of Other department student’s attendance
他学科聴講の条件
Conditions for Other department student’s attendance
人数に余裕があれば,聴講のみ可能
レベル
Level
2
キーワード
Keyword
プログラミング言語
型理論
論理学
定理証明
履修の際のアドバイス
Advice
発表をするときにしっかり事前に準備する必要がある.発表をしない日でも予習が必要.
授業開講形態等
Lecture format, etc.
基本的に対面で行う予定
遠隔授業(オンデマンド型)で行う場合の追加措置
Additional measures for remote class (on-demand class)
必要に応じてZoomなどで参加できる