证明与程序的类型

Collection Principles in Dependent Type Theory
Executing Higher Order Logic
A Tour with Constructive Real Numbers
An Implementation of Type：Type
On the Logical Content of Computational Type Theory：A Solution to Curry’S Problem
Constructive Reals in Coq：Axioms and Categoricity
A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals
A Kripke-style Model for the Admissibility of Structural Rules
Towards Limit Computable Mathematics
Formalizing the Halting Problem in a Constructive Type Theory
On the Proofs of Some Formally Unprovable Propositions and Prototype Proofs in Type Theory
Changing Data Structures in Type Theory：A Study of Natural Numbers
Elimination with a Motive
Generalization in Type Theory Based Proof Assistants
An Inductive Version of Nash-Williams'Minimal-Bad-Sequence Argument for Higman's Lemma
Author Index