论文标题
霍尔伯特：阅读，写作，证明和学习在浏览器中
Holbert: Reading, Writing, Proving and Learning in the Browser
论文作者
论文摘要
本文介绍了霍尔伯特：旨在教育用例的过程中的教学证明助手和在线教科书平台，特别是针对编程语言理论的教学。 Holbert允许将证明练习和规则定义直接嵌入在线教科书中，在线教科书可以使用图形接口来操纵证明和规则。我们概述了霍尔伯特的逻辑基础，其使用示例，并对其当前实施状态进行了更新。
This paper presents Holbert: a work-in-progress pedagogical proof assistant and online textbook platform, aimed at the educational use-case, specifically for the teaching of programming language theory. Holbert allows proof exercises and rule definitions to be embedded directly in an online textbook, where proofs and rules can be manipulated using a graphical interface. We give an overview of the logical foundations of Holbert, examples of its use, and give an update as to its current implementation status.
