Lambda encodings in type theory

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.