一本能在浏览器里直接运行的OCaml教材
作者为NPTEL慕课构建了一本完全在浏览器端运行的OCaml教材。通过x-ocaml和v86虚拟机技术，实现了零安装、零服务器的交互式编程体验。文章详细分享了从LLM辅助写作到自动化CI检查的工程实现细节，以及针对初学者的教学痛点解决方案。
评论
点赞
收藏OxCaml中的数据竞争自由：交互式验证并行程序
作者介绍如何在浏览器中嵌入基于OxCaml（Jane Street分支）的可编辑OCaml笔记本，并演示如何在不创建线程的情况下交互式地证明小型并行程序的数据竞争安全性。内容结合了教程和讲座笔记，展示了OxCaml在并行编程验证方面的实际应用能力。
从收敛到确信：RDTs的按钮式验证
作者提出对于复制数据类型，收敛性并不足以保证正确性，主张使用Agentic Proof-Oriented Programming来验证RDTs，以达成比收敛更强的复制感知线性一致性。
黑客入门：掌握OCaml系统编程的基础技能
文章探讨了如何获得参与OCaml这样复杂系统项目所需的底层计算机技能，包括命令行、编辑器、版本控制、构建系统、编译器、调试器和Bash脚本等。作者指出这些技能通常需要通过沉浸式的系统编程实践来获得，并讨论了如何弥补这些技能缺口。
OCaml语言的演进之路：从稳定性哲学到多核革命
OCaml核心维护者KC Sivaramakrishnan分享OCaml语言演进历程。文章强调OCaml通过“简单与稳定”实现长期繁荣，详细解析了动态数组功能从提案到合并的漫长讨论过程，以及多核支持（Effect Handlers和Domains）这一重大变革背后的学术严谨性与工程挑战。
测试 x-ocaml：将 OCaml 笔记本作为 Web 组件在浏览器端运行
作者实验将 OCaml 笔记本作为纯客户端 Web 组件运行，验证了其在浏览器中支持 OPAM 包、代码高亮、自动补全和类型提示等丰富编辑器功能的可能性。
OCaml中的线性与唯一性：为何单纯的唯一性不够用
文章探讨了OCaml中唯一性模式（uniqueness mode）的局限性，指出仅靠唯一性不足以优化，必须引入线性类型（linearity）概念才能使唯一性在实际工程中发挥作用。
行为类型中的唯一性模式
Jane Street 正在为 OCaml 开发行为类型系统扩展，其中包含模式（modes）来追踪值的属性如作用域、线程共享和别名。本文重点介绍唯一性模式（uniqueness mode），展示其如何通过追踪别名来消除某些运行时检查，从而提升系统编程的安全性和效率。
加入我的研究组：关于招聘与申请的建议汇总
IIT Madras教授KC Sivaramakrishnan总结其招聘建议，介绍其专注于编程语言抽象解决系统问题的研究组，涵盖RA、博士及本科生招募情况与期望。
OCaml的形式化验证垃圾回收器
IIT Madras等机构发表最新论文，首次实现了针对工业级语言OCaml的端到端形式化验证垃圾回收器。研究使用F和Low语言从底层构建可提取为C代码的验证GC，通过分层设计分离抽象正确性与内存安全，并在OCaml 4.14.1中集成测试，性能与标准GC相当。这是内存安全与高性能平衡的重要工程突破。
在时空维度上约束数据竞争
剑桥大学学者提出一种新的共享内存并行程序语义，主张即使在存在数据竞争的情况下，无竞争的程序部分仍应保持顺序执行语义（局部数据竞争自由）。论文提供了操作语义和公理化模型，并在OCaml中实现，评估显示在x86上无性能开销，ARM上仅约0.6%，平衡了内存模型的可理解性与性能。
Off-CPU 时间分析
介绍使用eBPF进行Off-CPU时间分析，以监控程序阻塞等待的时间，并提供了BCC工具的安装指引。
OCaml程序GDB调试入门指南
介绍如何使用GDB调试OCaml程序，包含编译和基础调试步骤示例。
通过Jupyter Notebook教授OCaml与Prolog
作者分享了在IIT Madras使用Jupyter Notebook教授OCaml和Prolog课程的经验，包括将传统Lisp替换为OCaml以及利用Notebook进行作业分发和自动评分的教学实践。
多核OCaml职位招聘
印度理工学院马德拉斯分校计算机系招聘多名研究软件工程师，负责开发多核OCaml并推动Tezos生态系统采用该技术。文章介绍了多核OCaml项目旨在为OCaml添加原生可扩展并发和共享内存并行支持。
使用 rr 确定性调试并发 GC 缺陷
作者分享使用 rr 记录重放工具调试 Multicore OCaml 并发垃圾回收器中非确定性 bug 的经验，解决了并发调试难题。
ML Family 2019 研讨会征稿启事
KC Sivaramakrishnan 作为程序委员会主席，发布了关于 2019 年 ML Family Workshop 的征稿通知。该研讨会将在 ICFP 会议期间举行，主要面向传统 ML 家族编程语言及相关领域的投稿。
在裸机 Shakti RISC-V 处理器上运行 OCaml
作者分享在IIT Madras RISE组使用OCaml构建Shakti RISC-V处理器安全应用的进展，利用MirageOS unikernel减少不安全C代码。
持续基准测试与征集测试用例
OCaml Labs 部署了 Multicore OCaml 的持续基准测试基础设施，目前结果均为单线程 x86-64 环境。作者分享了利用这些数据进行性能决策的经验，并呼吁社区贡献更多基准测试用例以优化多核运行时。
JFP特刊：代数效应与处理器的理论与实践
KC Sivaramakrishnan与Andrej Bauer正在编辑JFP关于代数效应和处理器的特刊，征稿截止至2019年1月18日。文章介绍了计算效应在现实语言中的重要性，如异常处理、并发等，并提供了投稿指南。