Dependently typed programming in Agda
Dependently typed programming in Agda
复制标题
Agda 中的依赖类型编程
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
U. Norell
中科院分区：
文献类型：
--
作者：
U. Norell
依赖类型语言长期以来一直被用来描述程序的证明。传统上，依赖类型主要用于陈述和证明程序的属性，而不是定义程序本身。一个令人印象深刻的例子是Leroy（2006）在Coq中实现并证明正确的认证编译器（Bertot和Castéran 2004）。
最近，人们对依赖类型编程的兴趣越来越大，其目的是编写更高程度地使用依赖类型系统的程序。通过这种方式，许多以前被单独证明的性质可以被集成到程序的类型中，在许多情况下，很少或没有增加程序定义的复杂性。新的语言，如Epigram（McBride and McKinna 2004），正在被设计，现有的语言正在被扩展新的功能来适应这些想法，例如Sozeau（2007）在Coq中的依赖类型编程。
这个演讲概述了Agda编程语言（Norell 2007），其主要重点是依赖类型编程。Agda提供了一组丰富的归纳类型，并提供了一个强大的模式匹配机制，允许以最小的麻烦编写依赖类型的程序。要阅读有关Agda编程的内容，请参阅高级函数式编程暑期学校的讲义（Norell 2008）以及Oury和Swierstra的工作（2008）。
在谈话中，一些有趣的依赖类型的程序从编程语言实现领域选择的例子，因为它们是在Agda实现。
Dependently typed languages have for a long time been used to describe proofs about programs. Traditionally, dependent types are used mostly for stating and proving the properties of the programs and not in defining the programs themselves. An impressive example is the certified compiler by Leroy (2006) implemented and proved correct in Coq (Bertot and Castéran 2004).
Recently there has been an increased interest in dependently typed programming, where the aim is to write programs that use the dependent type system to a much higher degree. In this way a lot of the properties that were previously proved separately can be integrated in the type of the program, in many cases adding little or no complexity to the definition of the program. New languages, such as Epigram (McBride and McKinna 2004), are being designed, and existing languages are being extended with new features to accomodate these ideas, for instance the work on dependently typed programming in Coq by Sozeau (2007).
This talk gives an overview of the Agda programming language (Norell 2007), whose main focus is on dependently typed programming. Agda provides a rich set of inductive types with a powerful mechanism for pattern matching, allowing dependently typed programs to be written with minimal fuss. To read about programming in Agda, see the lecture notes from the Advanced Functional Programming summer school (Norell 2008) and the work by Oury and Swierstra (2008).
In the talk a number of examples of interesting dependently typed programs chosen from the domain of programming language implementation are presented as they are implemented in Agda.