[05:16:23] *** Joins: drbean (~drbean@TC210-63-209-25.static.apol.com.tw) [10:25:52] daherb: is there a link to your talk today? [10:31:10] *** Quits: drbean (~drbean@TC210-63-209-25.static.apol.com.tw) (Ping timeout: 256 seconds) [10:46:20] oh wait you need tickets to that? [11:17:49] inariksit: the stream should be available here: https://streaming.media.ccc.de/rc3/hacc [13:07:10] *** Joins: drbean (~drbean@TC210-63-209-213.static.apol.com.tw) [13:14:30] inariksit no you do not. only for the 'interactive experience' you need tickets [13:14:52] (which is not properly working yet anyway) [14:47:50] *** Quits: drbean (~drbean@TC210-63-209-213.static.apol.com.tw) (Ping timeout: 265 seconds) [15:15:50] fl0_id: okay, I see! [16:59:29] watching now! [18:06:43] inariksit: how did you like it? [18:20:05] it was nice! nothing new to me really, but I imagine that a general audience interested in linguistics/logic learned a lot [18:21:55] i tried to formalize the montague languages in agda when preparing the talk but i got stuck [18:24:52] what does a language mean in this context? [18:26:32] I see stuff like ⟦⟧ in the code, is a montague language just that stuff you presented, with e and t, fancy brackets, rules how to apply stuff etc? [18:32:33] inariksit: i was following the "introduction to montague semantics" book. and they present languages in two versions, one purely logic language and one "english" version [18:32:46] e.g. L0 and l0E in my code [18:33:55] and it is both syntax, i.e. the types at the top and semantics, i.e. the [[]] and e's and t's