More.tex

\section{更多阅读}

\subsection{$\lambda$演算、类型论}


\emph{Syntax and Semantic of Lambda Calculus}, Henk Barendregt

\emph{The Impact of the Lambda Calculus in Logic and Computer Science}, Henk Barendregt

Martin-Lof’s (extensional) Intuitionistic Type Theory (1975): taking the proofs-as-programs correspondence
as foundational: a constructive formalism of inductive definitions that is both a logic
and a richly-typed functional programming language

Girard and Reynolds’ System F (1971): characterization of the provably total functions of secondorder
arithmetic

Coquand’s Calculus of Constructions (1984): extending system F into an hybrid formalism for
both proofs and programs (consistency = termination of evaluation)

Coquand and Huet’s implementation of the Calculus of Constructions (CoC) (1985)

Coquand and Paulin-Mohring’s Calculus of Inductive Constructions (1988): mixing the Calculus
of Constructions and Intuitionistic Type Theory leading to a new version of CoC called Coq

Coq 8.0 switched to the Set-Predicative Calculus of Inductive Constructions (2004): to be compatible
with classical choice


\subsection{数理逻辑和证明论}





\subsection{自动定理证明}


\subsection{Coq}
SF

CPDT

CoqArt