Document Type


Date of Degree

Summer 2014

Degree Name

PhD (Doctor of Philosophy)

Degree In

Computer Science

First Advisor

Stump, Aaron

First Committee Member

Tinelli, Cesare

Second Committee Member

Varadarajan, Kasturi

Third Committee Member

Herman, Ted

Fourth Committee Member

Jones, Douglas


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.


Church Encoding, Parigot Encoding, Scott Encoding, Type Theory


vi, 115 pages


Includes bibliographical references (pages 112-115).


Copyright 2014 Peng Fu