形式方法教程本教程将介绍编程语言理论中的一些基本主题。我们将通过为两种简单的编程语言构建解释器来实现这一点：Arith Lang和类型良好的lambda演算。依赖类型编程语言Idris将用于介绍这些概念。Arith Lang最初在一篇题为编程语言理论中的符号速成课程的博客文章中正式描述。在这里，我们将形式化与用Idris编写的解释器一起展示。

类型良好的lambda演算的解释器最初出现在Idris语言的教程中。在这里，我们向解释器提供了一些解释基本形式方法的附加材料。

那么，如果您对更多编程语言解释器感兴趣，可以看看Aquila Aquila编程语言解释器源码和C语言解释器。对于依赖类型的功能编程语言，您可能会对Idris dev和Idris的GRIN后端源码感兴趣。

贡献如果您想为本教程做出贡献，请随时这样做。但是，请先阅读有关的。可以在问题跟踪器中找到并归档问题。建造本教程使用LaTeX构建。Makefile可用于构建PDF。

探索这些资源，您将发现编程语言理论的奇妙世界，感受形式方法的魅力！