Document Type

Dissertation

Date of Degree

Summer 2014

Degree Name

PhD (Doctor of Philosophy)

Degree In

Computer Science

First Advisor

Aaron Stump

Abstract

Lambda encodings (such as Church encoding, Scott encoding and Parigot encoding) are methods to represent data in lambda calculus. Curry-Howard correspondence relates the formulas and proofs in intuitionistic logics to the types and programs in typed functional programming languages. Roughly speaking, Type theory (Intuitionistic Type Theory) formulates the intuitionistic logic in the style of typed functional programming language. This dissertation investigates the mechanisms to support lambda encodings in type theory. Type theory, for example, Calculus of Constructions(CC) does not directly support inductive data because the induction principle for the inductive data is proven to be not derivable. Thus inductive data together with inductive principle are added as primitive to CC, leading to several nontrivial extensions, e.g. Calculus of Inductive Constructions. In this dissertation, we explore alternatives to incorporate inductive data in type theory. We propose to consider adding an abstraction construct to the intuitionistic type to support lambda-encoded data, while still be able to derive the corresponding induction principle. The main benefit of this approach is that we obtain relatively simple systems, which are easier to analyze and implement.

Keywords

Church Encoding, Parigot Encoding, Scott Encoding, Type Theory

Pages

vi, 115 pages

Bibliography

Includes bibliographical references (pages 112-115).

Copyright

Copyright 2014 Peng Fu

Share

COinS