[logic-ml] talk by Chung-chieh Shan (15 May 2012)

[Hasegawa Masahito]

$B3'MM!"(B

$B0J2<$NFbMF$G(BChung-chieh Shan$B$5$s$N9V1i$rM=Dj$7$F$*$j$^$9!#(B
$B4X?4$r$*;}$A$NJ}$O!"@'Hs$*5$7Z$K$4;22C$/$@$5$$!#(B
$B$I$&$>$h$m$7$/$*4j$$$$$?$7$^$9!#(B

$BD9C+ at n???M(B
$B5~ETBg3X?tM}2r at O8&5f=j(B

--

$BF|;~(B	2012$BG/(B5$B7n(B15$BF|!J2P!K(B11:00$B!A(B12:00

$B>l=j(B	$B5~ETBg3XAm9g8&5f(B2$B9f4[!J5HED%-%c%s%Q%9K\It9=Fb!K(B4$B3,(B478$B9f<<(B
	Room 478, General Research Building No.2, Kyoto University
	(Access information & map:
	 http://www.kyoto-u.ac.jp/en/access
	 http://www.kurims.kyoto-u.ac.jp/~hassei/map-2.jpg )

$B9V1i<T(B	Chung-chieh Shan$B;a(B (Cornell$BBg(B/$BC^GHBg(B)

$BBj(B	Functional modularity in the lambda calculus

$B%"%V%9%H%i%/%H(B

 (I (B (I (BA module is a part of a _description_ of a system, not necessarily
 (I (B (I (Ba physical part. (I (BFor example, a program that is stored only in
 (I (B (I (Bcompiled form by the computer running it may nevertheless be better
 (I (B (I (Bdescribed by source code, so the program may have source modules
 (I (B (I (Bthat are hard to recover at run time. (I (BThis functional notion of
 (I (B (I (Bmodularity is relevant for organisms, species, and scientists
 (I (B (I (Bbecause they all need to adapt to changes in the environment without
 (I (B (I (Bre-learning, re-evolving, or re-discovering each new system from
 (I (B (I (Bscratch.

 (I (B (I (BLambda calculi and type systems offer expressive ways to describe
 (I (B (I (Bnatural language and thus carve out its modules. (I (BIn particular,
 (I (B (I (Blambda calculi can express modules that operate on other modules,
 (I (B (I (Band type systems can circumscribe information flow among modules
 (I (B (I (Bwhose operation is tightly intertwined. (I (BI will illustrate the use
 (I (B (I (Bof this expressivity with two examples: (I (BFirst, Abstract Categorial
 (I (B (I (BGrammars can carve out sound and meaning as a collection of modules
 (I (B (I (Bmediated by syntax. (I (BSecond, monad transformers can carve out side
 (I (B (I (Beffects such as continuations and state as a collection of modules
 (I (B (I (Bmediated by lexical items.

$B!JLd$$9g$o$;@h!'D9C+ at n!K(B

--
$BD9C+ at n???M(B <hassei at kurims.kyoto-u.ac.jp>
$B5~ETBg3X?tM}2r at O8&5f=j(B