equal
deleted
inserted
replaced
28 \item[\thydx{LCF}] is a version of Scott's Logic for Computable |
28 \item[\thydx{LCF}] is a version of Scott's Logic for Computable |
29 Functions, which is also implemented by the~{\sc lcf} |
29 Functions, which is also implemented by the~{\sc lcf} |
30 system~\cite{paulson87}. It is built upon classical~\FOL{}. |
30 system~\cite{paulson87}. It is built upon classical~\FOL{}. |
31 |
31 |
32 \item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an extension of |
32 \item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an extension of |
33 \texttt{HOL}\@. %FIXME See \cite{MNOS98} for more details on \texttt{HOLCF}. |
33 \texttt{HOL}\@. See \cite{MuellerNvOS99} for more details on \texttt{HOLCF}. |
34 |
34 |
35 \item[\thydx{CTT}] is a version of Martin-L\"of's Constructive Type |
35 \item[\thydx{CTT}] is a version of Martin-L\"of's Constructive Type |
36 Theory~\cite{nordstrom90}, with extensional equality. Universes are not |
36 Theory~\cite{nordstrom90}, with extensional equality. Universes are not |
37 included. |
37 included. |
38 |
38 |