溺潮112日 20241021
坏了、好久没有写，我们先补溺潮108日~111日的日志吧。
今天完成了 STLC 的 preservation 和 progress 证明。关于 normalization 的部分，可能要丢到之后再去写了，哎哎。
溺潮111日
林克阳来北京了，于是见他一面，去北海那边、特别是景山公园逛了会儿。
溺潮110日
急速完成了崩铁的版本活动，开心子。
溺潮109日
去开会、去上吉他课，学了击勾弦、闷音之类的！
溺潮108日
截稿后的第一天，狠狠写了 STLC 中关于 HashMap 的代码，真好啊
溺潮107日 20241016
持续一整天的压抑与不知道怎么办的赶稿、以及中午吃完饭后的彻底崩溃、哎、该怎么说呢。晚上7点多交了稿之后到现在、感觉都在瘫软、很难受啊。另外练了下那首曲子、的一点。哎。
溺潮106日
继续玉玉的一天以及略微改点、哎。但是竟然练了会儿琴、虽然那真的叫练琴吗？
溺潮105日 20241014
debug 不是很成功，只能是打包整理代码，然后继续改 paper 里的 evaluation 部分。哎、亲爱的导，你怎么直接重写了我的 introduction，对不起，我太菜了呜呜呜。
溺潮104日
考完试了，令人感叹。
溺潮103日
写了 Lean，感觉学会 pattern matching 了，真好玩啊
溺潮102日
去海关博物馆看了，哎，然后是写材料。
溺潮101日
复习考试。
溺潮100日 20241009
下午好好地、睡了一整个下午。晚上才来办公室加个班（
怎么会如此，好几天没写日记了，竟然也是溺潮百日了，补了98、99日的日记。简单debug一下吧、真的、我哭死。
我去！我竟然debug出来了，令人感叹啊令人感叹，循环支持、成功加入！
时至如今，不如下班收工！
溺潮99日
改了 abstract 和 introduction！呜呜呜，反正是、没有在办公室办公的一天。
溺潮98日
原神，启动！玩了一整天的5.0主线，十足拖延症。
练琴了，对caged音阶熟悉了一些？
溺潮97日
继续写论文，从 overview 中裂出一章 background 了，以及补充了 conclusion 部分，之后可能还得把 limitation, future works 加在附近，比较难想。还要对 abstract 和 introduction 进行全方面的修改，感觉到更严重的头疼了。
先，下班收工回去练琴吧、一点感叹。
溺潮96日
没有工作、也没有睡觉、是许久没有的纯粹过量娱乐，该怎么说呢。
溺潮95日
今日没有工作，睡了好久好久，感觉好了点。
晚上练了琴。然后感觉 love2000 的前奏可以硬啃一下，也就是2小节重复9次罢了（爆笑）170BPM对我来说，还有点太难了。
溺潮94日
改代码改得我有点不自信了，救命。
溺潮93日
evaluation section 写了一半大概？然后继续改code了，但是好像不怎么好，是精神不集中吗？怎么会写出这么错误的代码。然后状态确实不怎么好、哎、令人感叹了。
溺潮92日
10月的第一天、好好地睡到11点。
今天的工作主要是给代码debug，结果还没开始写 evaluation section 是吗？但是算是找到参考文章去模仿了，明天起床再写吧。虽然debug发现的结果都是几行能搞定的。等写完 eval sect 之后，可能还要再修改一下代码，有一个东西需要去支持，但是文本先写出来吧，这个太困扰了。
晚上回来练了琴，挺好的。虽然还是不熟悉，但是、就此迈向熟悉吧。
我感觉、在酝酿着溺潮的反题与合题，但是尚未能凝结出一个好的意象，于是就暂且先放下，会有时间做到的，至少在截稿之后，我会去休息一下。
溺潮91日
9月份竟然就要这么地结束了! 今天上午在深入熟悉 ECMTT，感觉还行，但是我还没发现啥新东西。
晚上整理了 paper 的 evaluation examples，但是要解决他们，还需要改改代码，希望没什么问题，code todo list已经写好了。然后另外惊喜的是，导师他真的，我哭死，在国庆前给了反馈，然后约了周三(10月2日)做针对性的讨论，他真的，我哭死x2。
好了，今天就先到这，下班收工！
溺潮90日
除了上课，仍然是无所事事的一天，除了、早晨练琴了。
溺潮89日
好累啊，去上课了。
溺潮88日
今天是开组会的一天。
晚上看了《看不见的朋友》，挺好的喵，还去被采访了（（
溺潮87日 20240926
今天读了 Contextual modal types for algebraic effects and handlers ，额，不知道该怎么评价了。对于 CMTT ，算是更了解了一些，然后这个工作是把 AlgEff 整合进 CMTT 的吧。哎、incremental work，估计就是 Alex 给学生的题目吧。这篇工作也承认自己没有涉及 effect theory，也就是那一堆的等价，那还能叫 AlgEff 吗（大家都这样叫是吧）终究还是没有人推进这个+DT的工作。
练了琴，哎。
溺潮86日
第二天才补的日记。相当于休息的一天。去学琴了，感觉要重新形成一些练习习惯。
溺潮85日
算是认真读了，一部分，Polynomial Time and Dependent Types。认真看了背景导入和related work。Section 456 跳得很快。这篇工作的主要贡献还是将多项式时间带到了 DT 的环境中去，这当然区分于 calf 那种额外的 program logic。对我而言，算是重新认识了 Martin Hofmann 的工作吧，LFPL，以及为了表明 soundness 与 completeness 的 realizability （这个我还不熟悉细节，因为需要仔细读 Section 6）。另外 formalization 里的 pho 表示 available usage，有些不太能理解，不过这个构建确实区别于 AARA 的 approach 吧。然后是 implicit/explicit annotation 的区别可能是？implicit 的 program quantitive behaviour 不需要任何的 explicit resource annotation. Future works 里指向的 synthetic computational complexity 我还挺感兴趣的，哎。就先读到这吧，有趣的论文，要不要bidding选这篇呢？
溺潮84日 20240923
新的一周，虽然没有开始阅读这周的论文，但是今天把代码中导致例子出问题的bug给修了，开心，于是，下班收工！
溺潮83日 20240922
今天写完了 paper proof。测试样例什么的留到下周吧。
练了琴，是好的。
溺潮82日 20240921
今天写了 paper proof 的最主要部分，发现一个难的点，想到深夜算是有新想法了，但是还没完成，可能明天还要再写一点。然后是测试样例，我感觉可以整出来一点了，但是有几个例子不知道为什么不行，下周要主力干这个。
哎！
溺潮81日
去上吉他课，感觉越发的困难，主要是我一直就不怎么跟节拍，这只能说是需要大量练习才能完成的。
溺潮80日
上午先练了会儿琴、哎、令人感叹。下午去和导狠狠聊天了，因而对接下来做什么更清晰了些。先写完 Implementation 吧，这个比较复杂一些。Lean formalization 先放下，先改一版 paper proof 可能。
溺潮79日
下午算是赶完了 Type Inference 以及 Soundness 的文本。文本上还缺 Implementation，Related Works 以及 Conclusion，感觉好累。而且还要在 Lean 里面去做 formalization，可恶，proof 先暂时别写，把文本攒出来再说！
哎哎、但是还是先写了会儿 proof，就差一点把第一个引理证出来，服了。
溺潮78日
Paper 修改润色了 Syntax 一章，哎，然后 Type Inference 刚开了个头。然后 formalization in Lean 还在思考ing，不是很会 Lean。但是今天是中秋，下班收工！
然后回去还是爆肝写了是吧、哎哎。
溺潮77日
看了 Deriving with Derivatives: Optimizing Incremental Fixpoints for Higher-Order Flow Analysis，我没看那个具体的 example，比较头疼，额，怎么说呢，这篇paper不是我所期望的来个 running example 讲解的，虽然我最后看懂了为啥起作用：与 workset algorithm 的区别在哪呢、是提供了一套框架吗？描述了哪些是可以 workset derivatives 去做而能 performant done 吗。哦哦哦哦哦，偏导数 partial v/partial x 会自动不去更新那些没有触发更新的变量 y。但是可能写得不是很好、我指的是把核心观点喂得舒服一些。Specializing Derivatives 这一部分涉及 partial eval，但是我还不怎么看得懂呜呜呜 似乎 pe 简化了 dependence ？？比起 workset 算法，在做一个 small-step 的 workset ，嗯，有点意思了。partial eval似乎有点dp的意思了，我们关联一下lilac吧（笑）总的来说，有意思的喵。
快速 Skim 了 Verus: Verifying Rust Programs using Linear Ghost Types 感觉比较有趣的就是 spec/proof/exec 三种 mode 的区分，然后利用了 Rust 的 linear borrow mechanism 来帮助证明，其余的似乎没有了，这一点可能主要体现在 proof 也能做 mutation 上，利用 borrow 来帮助翻译到 purely funcitonal code in Theorem Prover，哦，似乎是翻译到 CIC 上的。哎，不过 proof 可以 mutation 确实吸引人捏，有时候 pure fp 还挺烦人的，当然 spec 还是 pure fp 的。可能比较逆天的是在 Rust 里面写 proof 吧，哎、不得不令人感叹（因为某项目）
溺潮76日
今日不登校（x），算是休息了，虽然也有看 LEAN 相关的东西，但是我觉得我主要在做的事情是、抑制溺潮。正如罪漫最后变作我漫，我觉得这是辩证法的运动，溺潮中潜藏着的狂潮，应当被抑制吧，也就是说，溺潮的反题需要参与运动了。于是心态平和不少，明天应该能比较缓和地去工作了。第三周的论文阅读，以及继续写我的 paper，去做吧。
顺便、今日练琴了。
溺潮75日
久违了，早上的办公室。
晚上的总结：今天算是写完 overview 了，尝试写一下 formalization，有点难受啊，还不是很熟悉 LEAN。
感觉最近没怎么练琴，呜呜子。
溺潮74日
今天看了下 OOPSLA'25 的截止时间，是10月15日，决定去投这个，希望好运以及我能赶得上。
下午组会完了之后写了大概 1 页的 overview，2 小节，希望明天能不能写完剩下列好细纲的 3 小节。我们还得去润色技术细节部分，可能也要花不少时间。
溺潮73日
今天感觉还是挺懈怠地，不过想了 overview 大概怎么写，也开了个头，introduction 也补充了一些内容，对论文整体写作有了信心，只是需要时间。另外也整理了一点 latex 结构，之后该去狠狠调整了。内容量上应该还算够的吧，中间的 formalization 我还没有好好添加解说文字呢。
是练了琴才来写论文的，不过我感觉不太舒服，就是和弦转换之类的，不很连贯，比较烦；而且我也跟不上 Another Dime 的那个速度，快速切换左手，令人感叹，这也是要用右手带动左手吗？
溺潮72日
今天睡了几乎一整个白天，但是晚上p值爆棚，竟然写了下 paper，我觉得可以开始努力改论文了，部分来说启动了，目标是在下周四1-1 meeting之前，写出个初稿。
回去练琴了！
溺潮71日
今天吉他学了失真的几个和弦，以及一首新的旋律 Another Dime。然后是崩铁版本更新、哎、总感觉自己玩游戏日渐失去力气、像高中那样。
溺潮70日
还是得好好休息子呜呜呜，被噩梦死死控住。
Skim 了 Mechanizing Refinement Types ，感觉贡献在于 RefinementTypes+SemanticSubtyping+ParametricPoly，以及这个可以在 Liquid Haskell 里 mechanize ，也就是说，Refinement 这样原以为重的 verification 任务，不借助 proof-assistant 也可以完成验证，包括在 future works 里也希冀着用 LiquidHaskell 实现 SMT-solver with verification。这在 practical 上来说更适合 programming，没有 pa 那么重，比较 lightweight 吧。我没有细看其中所谓的 data proposition types，但是感觉就是 proof-term : proof-type 这种东西，一种 lightweight 的 dt. 想起暑假审稿的那篇 lightweight dt via staging。
现在还是细读这篇吧，不仅因为我对 refinement 感兴趣，而且我觉得他的写作结构也很值得学习。
内容上，他的 implications/predicate 是真的做了 non-SMT 的 mechanization 的，靠跑程序返回 Boolean 来确定，那这确实是 decidable 了，难怪 LiquidHaskell 的 mechanization 跑了 30 分钟。。。
溺潮69日
今天没有很正常地工作，不过对于我来说，一直处于不正常吧（笑）
Skim 了 Contextual Modal Type Theory，这是 08 年的 paper 了，很老。感觉 JohnSterling 的那个 MLTT-lock 就是后续衍生作吧，CMTT似乎没有让 necessity 在 dependent setting 下，也在 CMTT 的 future works 里看见了 dependent-necessity。
也 Skim 了 Modular Denotational Semantics for Effects with Guarded Interaction Trees ，这篇是对 Interaction Trees 的衍生作，似乎结合了 Guarded TT 与 Iris ，但是我不懂后两者，我就说说 ITrees ，这个我应该在2022年就Skim过，今年上半年的想法，似乎就是要用 ITrees 的样子，也就是那些可能不停机的程序。GITrees 这篇，整了 Higher Order functions/effects 这个，而香草(vanilla) ITrees 只能一阶，但是根据 related work 里说的，GITrees 不支持 extract 和 executable，这就让人感到恶心了吧，我最初喜欢（但是忘记了）ITrees 就是因为这个缘故，说不定是改进方向吧，单纯 reasoning 而没有 execution 果然还是不美。
Another difference worth mentioning, is that regular interaction trees can be extracted and executed from Coq. Our formalization cannot be directly extracted, as it is built upon a layer of guarded type theory.
然后这个从标题上就说 Denotational Semantics，根据我现在的印象，这下真是把 function (从 object-level) 拉到 meta-level 里了, Domain Theory 其实我不懂，完了，我怎么什么都不懂.
好了，今天就 Skim 到这，下班收工。
溺潮68日 20240907
头疼，感冒了应该是。
溺潮67日
去了三联的活动，以及今晚练琴了。
溺潮66日
Lilac 的那个 idea 果然有问题，没有那么简单，新想了一个版本，希望是正确的，不过即便如此，也就先这样放着吧，终止性虽然没问题，但是 modular 似乎还没那么简单，所以可以放一放。
昨晚因为这个以及没休息好的缘故，导致心情直接爆炸，没有练琴。
溺潮65日
早上改了一点项目代码，比较麻烦呢，输出格式，再改改然后暂时这么用着吧，代码可能还得再整理一下，然后跑多点测试例子才是重点，要为论文服务才行。
下午睡过去了，然后就是刚才去聚餐，哎，小学弟，怎么说喵，感觉我有点没带起来，他一个人坐在边角呜呜呜。
现在去练琴吧，还有洗澡。第一次剃须喵，好w
该规划一下周五的年轻人之夜了。
溺潮64日
Lilac 的那个新idea写了一点formalization，暂时还不是很确定是否能保证性质；
去看了《通往夏天的隧道，再见的出口》电影，感觉还挺好的，中等喜欢，限于83分钟的篇幅，我觉得很多细节不太能够到位吧，晚上和虎子哥去新东方阅读空间看到了实体小说，感觉有点差异，之后会去看看小说。我还是很爱这种异常性的小说，世界系吗？尽管很多恋爱桥段，几乎都是典中典了，我对虎子哥锐评这部电影时也是如此，因此我是中等喜欢而不是特别喜欢？但是女主的那句，我想去到你的世界，这样的想法，我还是很喜欢很喜欢的吧，时间流速差异导致的姐弟恋也是超绝（笑）。然后看的时候想到一个小点，延续着之前那个物理狂想的，关于神秘与确定的点：只有抛弃与你的最后的信物，我才能让你从确定复归不确定，只有这样，才能从迷雾中再次看见你。这样的先破后立，会是很棒的恋爱小说点子吧。我发觉我还是喜欢点子文学这一套，语不惊人死不休？郑渊洁害的。
下午学琴，被教了某个练习曲（BEAN SCENT）作为节奏练习，以及四组和弦的往返练习。我想，跟节拍器这点，还是往返地要重复，要用右手的节奏带动左手。
PS: 第二日才补的笔记，与虎子哥吃晚饭之后，或许一整天的奔波，还挺劳累的吧。
溺潮63日
今天继续来读 paper，是这篇 Capturing Types
感觉可以锐评 MoonBit 的 map:List[A] -> (A->B) -> List[B] 竟然不能支持 effects 了，即没办法 map:List[A] -> (A->B!E) -> List[B]!E，这篇paper可以解决相应的问题，并且保持 map 的签名仍为前者，感觉这个设计很棒。
这篇的contribution应该是提出了如何分析捕获变量以及变量逃逸，比较新颖的设计是引入了 Contextual Modal Type(Box/Unbox)，不让 capture sets 爆炸和不精确，2.x 的例子分析写得很棒。
Cap hierarchy 似乎比 row poly 要更舒服一点，cap sets 可以做得比较小。
Lilac 想到了个新的东西，开心子。
练琴的话，感觉稍微熟练了点，自己的意识也更好了些，主要是后者喵。
溺潮62日 20240901
怎么就9月了，哎。
上午看了 A Core Calculus for Documents: Or, Lambda: The Ultimate Document, 简单锐评两句，感觉构造比较复杂，但是那个 strtpl(string-template) 的branch 比较清楚了，涉及 set x = e 在 template 里面怎么处理，这里直接抽象出来一个 template list，在做 interpretation(文中称之为 desugaring, 额，行吧) 做一个特化, 大概形如下述:
(| set x = e :: tl |)_desugar = let x = e in (| tl |)_desugar然后其他的各种variant branch差不多，啥treetpl, reference, reforest 之类的，然后 reactive (响应式) 的都能在这套 doc calculus 上面做，大概是这么个思路，这个 interpretation 大概是分为了2层？这个let x = e 范式的就是这么嵌进去的，服了，因此我也想到和 staging 的关联吧，大概？语义上相似，语法上（指quasiquote）也相似。
然后可能总结一下这篇paper的contribution？感觉总结了一大类（就Table 1的8种情形，像 x=${x} 、Markdown 与 Typst），给了一个很好的 formalizaiton；然后还给了一个 type system for template(5.1) ，这里其实我也觉得是最 staging 的吧，对 staged-expression 的 typing 呗（笑），但是作者没这么显式说；reactive 与 reference 的 local/global 也有趣，还有 dirty update 相关的讨论，不过我还不是很清楚具体细节，就先读到这吧。PS: reforestation 也有意思，语义(desugaring) 跟 set x = e 的形式比较像。
评价就是，我觉得工作很充分，但是要说有什么 novelity？我不确定，或许前面确实没有人做过相关的工作吧（草）。这里与 pretty printing 的关系我觉得也是可以延申一下的，我觉得像啊，很像啊，这个 staging 的 semantics/desugaring。
哎，下午 lilac 继续，然后晚上练琴，洗澡游戏！练琴感觉，要连贯流畅确实是一个很需要练习的地方呢！
溺潮61日
今天睡了很久，出门去麦麦吃好吃的了，吃了之后回办公室把项目的bug给搞清楚了，哎，永远都会被typo杀死吗？
吃晚饭后报修了下马桶，怎么塞住了，烦捏，然后练习了一小时的琴，难受子，记不住降八度升八度的位置在哪里，怎样才能更快地记住呢，条件反射般地期望。现在准备洗澡洗头和玩游戏啦~
溺潮60日 20240830
夏末了，但是突然变热、33℃，北京这是怎么了，久违地再开空调，中午睡觉时就感觉有点热，但是还没反应过来就睡着了。
溺潮59日
狠狠地继续写 lilac，应该说这样的才配得上溺潮的观感？但是也太过了吧，以至于没有练习吉他，日常练习还是得做。
溺潮58日
吉他练习了，然后写了lilac的notes，越写越上头喵，打算用Rust重写了。
溺潮57日 20240827
今天去学了吉他的第一节课，要去弹音阶了，一个要背熟音符在吉他上的位置，另一个是具体操作上的，左手要按住喵，按稳了喵。另外是，我似乎跟节拍还是不太行，之后还得练习一下子。
另外今日狂飙式补原神4.8的版本活动，可惜，最后只能拿了绮良良的皮肤，而角色本体没法拿到，对于萌新来说太难了，没有练度。
关于工作，明天应该要进行吧、感叹。