2010 Formosan Summer School on Logic, Language, and Computation (FLOLAC '10)
http://flolac.iis.sinica.edu.tw/flolac10/
2011-03-15T06:42:14+08:002010 Formosan Summer School on Logic, Language, and Computation (FLOLAC '10)
http://flolac.iis.sinica.edu.tw/flolac10/
http://flolac.iis.sinica.edu.tw/flolac10/lib/images/favicon.icotext/html2010-07-08T15:14:14+08:00deno
http://flolac.iis.sinica.edu.tw/flolac10/doku.php?id=deno&rev=1278573254&do=diff
Lecturers: 莊庭瑞 Tyng-Ruey Chuang.
The purpose of this course is to equip students with some knowledge about basic domain theory, and about denotational semantics of functional programs and While programs.
Course Materials
* [Lecture notes (2010-07-08 updated)].
* [Slides (2010-07-08 updated)].
* [In-class exercise.]
* [homework.]
* [Another In-class exercise (new).]text/html2010-06-29T06:34:53+08:00fp
http://flolac.iis.sinica.edu.tw/flolac10/doku.php?id=fp&rev=1277764493&do=diff
Lecturer: Tyng-Ruey Chuang 莊庭瑞
The purpose of this course is to equip students with knowledge of functional programming using the Objective Caml language.
None. Each student must has her/his own labtop to work on programming assignments.text/html2010-06-27T18:56:44+08:00frama-c
http://flolac.iis.sinica.edu.tw/flolac10/doku.php?id=frama-c&rev=1277636204&do=diff
Lecturer: Pascal Cuoq.
Frama-C is a framework for combining analysis techniques towards the analysis or verification of C code.
Why C? C is widely use for embedded programming. In a tiny number of cases, the embedded software is critical: lives depend on it functioning as expected. These applications do, and will increasingly, take advantage of formal methods.text/html2010-07-08T22:18:21+08:00logic
http://flolac.iis.sinica.edu.tw/flolac10/doku.php?id=logic&rev=1278598701&do=diff
Lecturers: 謝邁思 Max Schäfer.
This lecture aims to provide students with the logical background knowledge needed to understand and appreciate the other lectures. We will cover propositional and first-order classical logic, both from a semantic perspective and in the context of sequent calculus. Time permitting we will also take a brief look at logic programming in Datalog.text/html2010-02-22T15:19:56+08:00menu1
http://flolac.iis.sinica.edu.tw/flolac10/doku.php?id=menu1&rev=1266823196&do=diff
* 首頁
* 課程與講者
* 報名資訊text/html2010-07-09T10:35:57+08:00menu2
http://flolac.iis.sinica.edu.tw/flolac10/doku.php?id=menu2&rev=1278642957&do=diff
* 邏輯
* 函數編程
* 操作語意
* 指稱語意
* 程式建構與推理
* 使用 Frama-C
* 研究討論text/html2010-07-06T15:44:31+08:00op
http://flolac.iis.sinica.edu.tw/flolac10/doku.php?id=op&rev=1278402271&do=diff
Lecturer: 陳恭 Kung Chen.
The aim of this unit will be to introduce the operational approach to programming language semantics.
It will show how this formalism is used to specify the meaning of some simple programming language constructs and to reason formally about semantic properties of programs.text/html2010-07-04T12:45:29+08:00prog
http://flolac.iis.sinica.edu.tw/flolac10/doku.php?id=prog&rev=1278218729&do=diff
Lecturer: 穆信成 Shin-Cheng Mu
This course gives an introduction to derivation and verification of imperative programs using Hoare Logic and Dijkstra's weakest precondition calculus. After learning how to verify the correctness of a program by checking the validity of its Hoare triple annotation, we introduce a systematic approach to program construction and problem solving by discovering possibly useful loop invariants. It is emphasized that a program and its correctness proof shall be constructe…text/html2010-06-13T18:54:31+08:00programme-temp
http://flolac.iis.sinica.edu.tw/flolac10/doku.php?id=programme-temp&rev=1276426471&do=diff
課表
6/28 6/29 6/30 7/1 7/2 7/5 7/6 7/7 7/8 7/9 Mon Tue Wed Thu Fri Mon Tue Wed Thu Fri 09:30 - 10:30 FP Logic Op Logic Prog Deno Deno Deno Exam 10:30 - 11:30 FP Logic Op Logic Prog Deno Deno Deno Exam 11:30 - 12:30 L/T L/T L/T L/T L/T L/T L/T L/T Exam 12:30 - 2:00 Lunch Lunch …text/html2010-06-25T09:12:17+08:00programme
http://flolac.iis.sinica.edu.tw/flolac10/doku.php?id=programme&rev=1277428337&do=diff
* 日期: 2010 年六月廿八日(週一)至七月九日(週五)。
* 時間: 每週一至週五早上九點至下午五點,依課程排定時間上課。
* 地點: 國立台灣大學進修推廣部 2 樓 207 教室(台北市106羅斯福路4段107號)。text/html2010-05-17T10:48:22+08:00registration
http://flolac.iis.sinica.edu.tw/flolac10/doku.php?id=registration&rev=1274064502&do=diff
* 報名資格
* 資訊、電機、數學相關學系在學大學生,修業兩年(含)以上,或
* 資訊、電機、數學相關學系研究所在學學生,或
* 專科或大學畢業,現從事資訊相關行業工作者。text/html2010-06-14T10:18:03+08:00start
http://flolac.iis.sinica.edu.tw/flolac10/doku.php?id=start&rev=1276481883&do=diff
暨「高等程式語言:語意、分析與工具」 (Advanced Programming Languages: Semantics, Analyses, and Tools) 暑期課程碩士學分班。
Array
* 課程網頁
近年來,從事基礎計算科學研究之台灣學者們已在各校各自成立研究團隊並相互合作。對基礎計算科學有興趣之學生須透過一系列課程學習基本知識。然而,國內從事此類研究的學者分散在各校,難以僅靠一己之力開設整套課程。因此,我們邀請有相同興趣的學者一同開課,訓練下一代的研究人才。…