[ 京都大学 | 数理解析研究所 | 関数型言語 ] ......................

Theories of Types and Proofs (TTP) - Kyoto Meeting

東京のTTPワークショップ(東京, 9月8-18日) と TACS (仙台, 9月23-26日) の狭間に, このワークショップは型理論, 論理, 応用と関連分野(プログラミング言語, 定理証明器などを含む)などについて自由に討論する場を提供します. ワークショップへの参加は自由です.

(本研究集会の元の名前は型理論とそのコンピュータシステムへの応用でした. 開催期間の変更にもご注意ください)

会場: 4階420号室; 京都大学数理解析研究所 (農学部キャンパス内)
〒606 京都市左京区北白川追分町
交通: 市バス203号(地下鉄今出川駅より)・11号(四条より)・17号(京都駅より)
北白川または農学部前下車
世話人: Jacques Garrigue
E-mail garrigue@kurims.kyoto-u.ac.jp
Tel (075)753-7211 FAX (075)752-7272
TTP-Kyoto プログラム委員: Jacques Garrigue (京都大学)
立木秀樹 (京都産業大学)
横内寛文 (群馬大学)
URL:: http://wwwfun.kurims.kyoto-u.ac.jp/ttp-kyoto/

下記のURLでTTP-TokyoとTACSに関する情報にアクセスできます.

プログラム

11:00～11:30: 松岡聡 (名工大・工); Towards a Higher Order Unification based on Proof Nets
11:30～12:10: Mario Coppo (Universita di Torino); Recursive Types: the Syntactic and Semantic Approach
14:00～14:40: 岡田光弘 (慶応大・文); 浜野正浩 ( '' ); Type-Theoretic Completion from Algebraic Specifications
14:40～15:20: Mariangiola Dezani (東工大・Universita di Torino); A Filter Model for Mobile Processes
15:50～16:30: 亀山幸義 (京大・工); Strong Normalizability of Classical Catch/Throw Calculus
16:30～17:10: Benjamin Werner (INRIA-Rocquencourt); Bruno Barras ( '' ); Towards Certified Proof-checkers
17:10～17:50: Philippa Gardner (University of Cambridge); Andrew Barber, 長谷川真人, Gordon Plotkin; From Action Calculi to Linear Logic

10:50～11:30: 照井一成 (慶応大・文); 岡田光弘 ( '' ); Some Semantics of Linear Logic (tentative title)
11:30～12:10: Giorgio Ghelli (Universita di Pisa); Complexity of Kernel Fun Subtype Checking
14:00～14:40: 橋本政朋 (京大・数研); 大堀淳 ( '' ); A Typed Context Calculus
14:40～15:20: Didier Remy (INRIA-Rocquencourt); Object Extension Unifies Objects with Classes
15:50～16:30: 赤間陽二 (東大・理); Intersection Typing System and Partial Combinatory Algebras
16:30～17:10: Erik Poll (University of Kent); Subtyping and Inheritance for Inductive Types
18:30～: 懇親会 (みそら)

9:30～10:10: 西村進 (京大・数研); Static Typing for Dynamic Messages
10:10～10:50: 香川考司 (香川大・工); Simplification of Subtyping Constraints and Its Application
10:50～11:30: 南出靖彦 (京大・数研); A Functional Representation of Data Structures with a Hole

JG 97.12.24.