没有合适的资源?快使用搜索试试~ 我知道了~
首页Type Theory & Functional Programming
资源详情
资源推荐
![](https://csdnimg.cn/release/download_crawler_static/10828759/bg1.jpg)
Type Theory & Functional
Programming
Simon Thompson
Computing Laboratory, University of Kent
March 1999
c
Simon Thompson, 1999
Not to be reproduced
![](https://csdnimg.cn/release/download_crawler_static/10828759/bg2.jpg)
i
![](https://csdnimg.cn/release/download_crawler_static/10828759/bg3.jpg)
ii
To my parents
![](https://csdnimg.cn/release/download_crawler_static/10828759/bg4.jpg)
Preface
Constructive Type theory has be en a topic of research interest to computer
scientists, mathematicians, logicians and philosophers for a number of years.
For computer scientists it provides a framework which brings together logic
and programming languages in a most elegant and fertile way: program
development and verification can proceed within a single system. Viewed
in a different way, type theory is a functional programming language with
some novel features, such as the totality of all its functions, its expressive
type system allowing functions whose result type depends upon the value
of its input, and sophisticated modules and abstract types whose interfaces
can contain logical assertions as well as signature information. A third
point of view emphasizes that programs (or functions) can be extracted
from proofs in the logic.
Up until now most of the material on type theory has only appeared in
proceedings of conferences and in research papers, so it seems appropriate
to try to set down the current state of development in a form accessible to
interested final-year undergraduates, graduate students, research workers
and teachers in computer science and related fields – hence this book.
The book can be thought of as giving both a first and a second course in
type theory. We begin with introductory material on logic and functional
programming, and follow this by presenting the system of type theory itself,
together with many examples. As well as this we go further, looking at
the system from a mathematical pe rspective, thus elucidating a number
of its important properties. Then we take a critical look at the profusion
of suggestions in the literature about why and how type theory could be
augmented. In doing this we are aiming at a moving target; it must be
the case that further developments will have been made before the book
reaches the press. Nonetheless, such an survey can give the reader a much
more developed sense of the potential of type theory, as well as giving the
background of what is to come.
iii
![](https://csdnimg.cn/release/download_crawler_static/10828759/bg5.jpg)
iv PREFACE
Outline
It see ms in order to give an overview of the book. Each chapter begins with
a more detailed introduction, so we shall be brief here. We follow this with
a guide on how the book might be approached.
The first three chapters survey the three fields upon which type theory
depends: logic, the λ-calculus and functional programming and construc-
tive mathematics. The surveys are short, establishing terminology, notation
and a general context for the discussion; pointers to the relevant literature
and in particular to more detailed intro ductions are provided. In the second
chapter we discuss some issues in the λ-calculus and functional program-
ming which suggest analogous questions in type theory.
The fourth chapter forms the focus of the book. We give the formal
system for type theory, developing examples of both programs and proofs
as we go along. These tend to be short, illustrating the construct just
introduced – chapter 6 contains many more examples.
The system of type theory is complex, and in chapter which follows we
explore a number of different aspects of the theory. We prove certain results
about it (rather than using it) including the important facts that programs
are terminating and that evaluation is deterministic. Other topics examined
include the variety of equality relations in the system, the addition of types
(or ‘universes’) of types and some more technical points.
Much of our understanding of a complex formal system must derive
from out using it. Chapter six covers a variety of examples and larger
case studies. From the functional programming point of view, we choose to
stress the differences between the system and more traditional languages.
After a lengthy discussion of recursion, we look at the impact of the quan-
tified types, especially in the light of the universes added above. We also
take the opportunity to demonstrate how programs can be extracted from
constructive proofs, and one way that imperative programs c an be seen as
arising. We conclude with a survey of examples in the relevant literature.
As an aside it is worth saying that for any formal system, we can really
only understand its precise details after attempting to implement it. The
combination of symbolic and natural language used by mathematicians is
surprisingly suggestive, yet ambiguous, and it is only the discipline of having
to implement a system which makes us look at some aspects of it. In the
case of T T , it was only through writing an implementation in the functional
programming language Miranda
1
that the author came to understand the
distinctive role of assumptions in T T , for instance.
The system is expressive, as witnessed by the previous chapter, but
are programs given in their most natural or efficient form? There is a
1
Miranda is a trade mark of Research Software Limited
剩余377页未读,继续阅读
![](https://profile-avatar.csdnimg.cn/default.jpg!1)
baozii
- 粉丝: 0
- 资源: 9
上传资源 快速赚钱
我的内容管理 收起
我的资源 快来上传第一个资源
我的收益
登录查看自己的收益我的积分 登录查看自己的积分
我的C币 登录后查看C币余额
我的收藏
我的下载
下载帮助
![](https://csdnimg.cn/release/wenkucmsfe/public/img/voice.245cc511.png)
会员权益专享
最新资源
- 计算机系统基石:深度解析与优化秘籍
- 《ThinkingInJava》中文版:经典Java学习宝典
- 《世界是平的》新版:全球化进程加速与教育挑战
- 编程珠玑:程序员的基础与深度探索
- C# 语言规范4.0详解
- Java编程:兔子繁殖与素数、水仙花数问题探索
- Oracle内存结构详解:SGA与PGA
- Java编程中的经典算法解析
- Logback日志管理系统:从入门到精通
- Maven一站式构建与配置教程:从入门到私服搭建
- Linux TCP/IP网络编程基础与实践
- 《CLR via C# 第3版》- 中文译稿,深度探索.NET框架
- Oracle10gR2 RAC在RedHat上的安装指南
- 微信技术总监解密:从架构设计到敏捷开发
- 民用航空专业英汉对照词典:全面指导航空教学与工作
- Rexroth HVE & HVR 2nd Gen. Power Supply Units应用手册:DIAX04选择与安装指南
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035111.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)