2010 Formosan Summer School on Logic, Language, and Computation (FLOLAC '10) http://flolac.iis.sinica.edu.tw/flolac10/ 2011-03-15T06:42:14+08:00 2010 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.ico text/html 2010-07-08T15:14:14+08:00 deno 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/html 2010-06-29T06:34:53+08:00 fp 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/html 2010-06-27T18:56:44+08:00 frama-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/html 2010-07-08T22:18:21+08:00 logic 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/html 2010-02-22T15:19:56+08:00 menu1 http://flolac.iis.sinica.edu.tw/flolac10/doku.php?id=menu1&rev=1266823196&do=diff * 首頁 * 課程與講者 * 報名資訊 text/html 2010-07-09T10:35:57+08:00 menu2 http://flolac.iis.sinica.edu.tw/flolac10/doku.php?id=menu2&rev=1278642957&do=diff * 邏輯 * 函數編程 * 操作語意 * 指稱語意 * 程式建構與推理 * 使用 Frama-C * 研究討論 text/html 2010-07-06T15:44:31+08:00 op 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/html 2010-07-04T12:45:29+08:00 prog 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/html 2010-06-13T18:54:31+08:00 programme-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/html 2010-06-25T09:12:17+08:00 programme http://flolac.iis.sinica.edu.tw/flolac10/doku.php?id=programme&rev=1277428337&do=diff * 日期: 2010 年六月廿八日(週一)至七月九日(週五)。 * 時間: 每週一至週五早上九點至下午五點,依課程排定時間上課。 * 地點: 國立台灣大學進修推廣部 2 樓 207 教室(台北市106羅斯福路4段107號)。 text/html 2010-05-17T10:48:22+08:00 registration http://flolac.iis.sinica.edu.tw/flolac10/doku.php?id=registration&rev=1274064502&do=diff * 報名資格 * 資訊、電機、數學相關學系在學大學生,修業兩年(含)以上,或 * 資訊、電機、數學相關學系研究所在學學生,或 * 專科或大學畢業,現從事資訊相關行業工作者。 text/html 2010-06-14T10:18:03+08:00 start http://flolac.iis.sinica.edu.tw/flolac10/doku.php?id=start&rev=1276481883&do=diff 暨「高等程式語言:語意、分析與工具」 (Advanced Programming Languages: Semantics, Analyses, and Tools) 暑期課程碩士學分班。 Array * 課程網頁 近年來,從事基礎計算科學研究之台灣學者們已在各校各自成立研究團隊並相互合作。對基礎計算科學有興趣之學生須透過一系列課程學習基本知識。然而,國內從事此類研究的學者分散在各校,難以僅靠一己之力開設整套課程。因此,我們邀請有相同興趣的學者一同開課,訓練下一代的研究人才。…