【零分作文】别样的函数式语言大战
Description
原作：BV1zK4y1x7sz 参考文献： Pierce, B. C., Casinghino, C., Gaboardi, M., Greenberg, M., Hriţcu, C., Sjöberg, V., & Yorgey, B. (2010). Software foundations. Norrish, M., Slind, K., Amjad, H., Brandt, J., Fox, A., Gordon, M., Homeier, P., Hurd, J., Tian, C., & Weber, T. (2024). The HOL system. 致谢：BV1JmKqzqENv BV1Wsu7zaEH8
Comments
别样的忘忧北萱草👍🏻
♥ 176 ↩ 6
❎ PLDI'25 ✅ PJSK'25 時 Lean 4 当然是一种小而美，beyond 证明助手大战！
♥ 127 ↩ 1
lean学长这招太狠了
♥ 60
Haskell这招太狠了[笑哭]
♥ 41
我们可爱的 Agda 小鸟呢 [颂乐人偶_眯眼笑]
♥ 36 ↩ 1
帮浙大老师推广推广，这是真的定理证明大赛[笑哭][笑哭]
♥ 25
PLD1 没绷住，up主也是五字神人
♥ 18
原来这种语言是可以证明实数理论的，好神奇，实数的定义是柯西列，光表示一个实数我都不知道该怎么办如果你的内存是有限的。
♥ 14 ↩ 33
亲自配音太草了吧[doge]
♥ 11
别样的势大力沉[支持]
♥ 10
看了看内容，看了看up的简介，恍然大悟了
♥ 8
太可爱了
♥ 7 ↩ 1
别样的[打call]
♥ 6
草，听你的声音太出戏了
♥ 6
交互式定理证明这一块[笑哭]
♥ 4
不兑，这怎么是隔壁学校动漫社。
♥ 4 ↩ 1
@弗熊你懂函数式编程吗
♥ 2 ↩ 1
破案了，批改作文的是lean
♥ 1
[范式起源_蓝的盆][范式起源_蓝的盆][范式起源_蓝的盆]
♥ 1
还有参考文献
♥ 1