KC Sivaramakrishnan

RSS: https://kcsrk.info/atom.xml
KC Sivaramakrishnan——可扩展函数式编程。

可运行的教科书

<p>这是我于2026年9月26日在班加罗尔举行的IndiaFOSS 6.0演讲的书面版本。幻灯片可作为以及.</p><figure> </figure><p>我想告诉你我为NPTEL课程写的那本书的故事,<em>使用OCaml的函数式编程</em>.首轮课程正在进行中,共有1,227名学生注册。该校浏览器运行:学生可以在页面中更改并直接执行示例,无需安装。</p><p>搭建它也让我学到了与编程代理合作的经验。代理在构建平台方面表现不错。写出学生能学习的材料则需要更多工作。</p><h2>一门我永远不会遇到的学习者课程</h2><figure> </figure><p>对于不熟悉这是一个在线课程平台,主要来自印度理工学院(IIT)和印度科学研究院(IISc)。讲座视频免费提供,包括YouTube。<br><br>学生还可以参加监考考试以获得认证,许多高校认可NPTEL课程学分。</p><figure> </figure><p>我认为NPTEL是印度学术界最伟大的集体成就之一。有优秀教师开设的基础课程。今年早些时候,我注意到它没有OCaml课程,于是决定开设一门。</p><figure> </figure><p>编程语言是通过点敲它们来学的。你修改程序,运行它,看看会发生什么。我怎么可能给1227个学生一个可用的OCaml环境?</p><p>这些学生分布在印度各地。有些人可能共用一台电脑;有些人可能没有自己的电脑。他们使用不同的操作系统,对机器的熟悉程度不同,网络可能不稳定。<br><br>还有一些学员会在本课程结束后很长时间观看视频。</p><p>录制NPTEL讲座意味着坐在一个小录音室里,对着摄像机讲话。我有两位非常…</p>
评论点赞收藏4 天前

一本能在浏览器里直接运行的OCaml教材

作者为NPTEL慕课构建了一本完全在浏览器端运行的OCaml教材。通过x-ocaml和v86虚拟机技术,实现了零安装、零服务器的交互式编程体验。 文章详细分享了从LLM辅助写作到自动化CI检查的工程实现细节,以及针对初学者的教学痛点解决方案。
评论点赞收藏107 天前

OxCaml中的数据竞争自由:交互式验证并行程序

作者介绍如何在浏览器中嵌入基于OxCaml(Jane Street分支)的可编辑OCaml笔记本,并演示如何在不创建线程的情况下交互式地证明小型并行程序的数据竞争安全性。 内容结合了教程和讲座笔记,展示了OxCaml在并行编程验证方面的实际应用能力。
评论点赞收藏146 天前

从收敛到确信:RDTs的按钮式验证

作者提出对于复制数据类型,收敛性并不足以保证正确性,主张使用Agentic Proof-Oriented Programming来验证RDTs,以达成比收敛更强的复制感知线性一致性。
评论点赞收藏155 天前

黑客入门:掌握OCaml系统编程的基础技能

文章探讨了如何获得参与OCaml这样复杂系统项目所需的底层计算机技能,包括命令行、编辑器、版本控制、构建系统、编译器、调试器和Bash脚本等。 作者指出这些技能通常需要通过沉浸式的系统编程实践来获得,并讨论了如何弥补这些技能缺口。
评论点赞收藏324 天前

OCaml语言的演进之路:从稳定性哲学到多核革命

OCaml核心维护者KC Sivaramakrishnan分享OCaml语言演进历程。文章强调OCaml通过“简单与稳定”实现长期繁荣,详细解析了动态数组功能从提案到合并的漫长讨论过程,以及多核支持(Effect Handlers和Domains)这一重大变革背后的学术严谨性与工程挑战。
评论点赞收藏390 天前

行为类型中的唯一性模式

Jane Street 正在为 OCaml 开发行为类型系统扩展,其中包含模式(modes)来追踪值的属性如作用域、线程共享和别名。本文重点介绍唯一性模式(uniqueness mode),展示其如何通过追踪别名来消除某些运行时检查,从而提升系统编程的安全性和效率。
评论点赞收藏489 天前

OCaml的形式化验证垃圾回收器

IIT Madras等机构发表最新论文,首次实现了针对工业级语言OCaml的端到端形式化验证垃圾回收器。研究使用F和Low语言从底层构建可提取为C代码的验证GC,通过分层设计分离抽象正确性与内存安全,并在OCaml 4.14.1中集成测试,性能与标准GC相当。 这是内存安全与高性能平衡的重要工程突破。
评论点赞收藏580 天前

在时空维度上约束数据竞争

剑桥大学学者提出一种新的共享内存并行程序语义,主张即使在存在数据竞争的情况下,无竞争的程序部分仍应保持顺序执行语义(局部数据竞争自由)。 论文提供了操作语义和公理化模型,并在OCaml中实现,评估显示在x86上无性能开销,ARM上仅约0.6%,平衡了内存模型的可理解性与性能。
评论点赞收藏655 天前

Off-CPU 时间分析

介绍使用eBPF进行Off-CPU时间分析,以监控程序阻塞等待的时间,并提供了BCC工具的安装指引。
评论点赞收藏798 天前

通过Jupyter Notebook教授OCaml与Prolog

作者分享了在IIT Madras使用Jupyter Notebook教授OCaml和Prolog课程的经验,包括将传统Lisp替换为OCaml以及利用Notebook进行作业分发和自动评分的教学实践。
评论点赞收藏2446 天前

多核OCaml职位招聘

印度理工学院马德拉斯分校计算机系招聘多名研究软件工程师,负责开发多核OCaml并推动Tezos生态系统采用该技术。文章介绍了多核OCaml项目旨在为OCaml添加原生可扩展并发和共享内存并行支持。
评论点赞收藏2571 天前

ML Family 2019 研讨会征稿启事

KC Sivaramakrishnan 作为程序委员会主席,发布了关于 2019 年 ML Family Workshop 的征稿通知。该研讨会将在 ICFP 会议期间举行,主要面向传统 ML 家族编程语言及相关领域的投稿。
评论点赞收藏2718 天前

持续基准测试与征集测试用例

OCaml Labs 部署了 Multicore OCaml 的持续基准测试基础设施,目前结果均为单线程 x86-64 环境。作者分享了利用这些数据进行性能决策的经验,并呼吁社区贡献更多基准测试用例以优化多核运行时。
评论点赞收藏2939 天前

登录芦苇

登录后关注作者、收藏内容和参与讨论。