117 \newblock {\em The {PVS} specification language}, |
117 \newblock {\em The {PVS} specification language}, |
118 \newblock Computer Science Laboratory, SRI International, Menlo Park, CA, Apr. |
118 \newblock Computer Science Laboratory, SRI International, Menlo Park, CA, Apr. |
119 1993, |
119 1993, |
120 \newblock Beta release |
120 \newblock Beta release |
121 |
121 |
122 \bibitem{paulin92} |
122 \bibitem{paulin-tlca} |
123 Paulin-Mohring, C., |
123 Paulin-Mohring, C., |
124 \newblock Inductive definitions in the system {Coq}: Rules and properties, |
124 \newblock Inductive definitions in the system {Coq}: Rules and properties, |
125 \newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon, Dec. |
125 \newblock In {\em Typed Lambda Calculi and Applications\/} (1993), M.~Bezem |
126 1992 |
126 J.~Groote, Eds., LNCS 664, Springer, pp.~328--345 |
127 |
127 |
128 \bibitem{paulson-markt} |
128 \bibitem{paulson-markt} |
129 Paulson, L.~C., |
129 Paulson, L.~C., |
130 \newblock Tool support for logics of programs, |
130 \newblock Tool support for logics of programs, |
131 \newblock In {\em Mathematical Methods in Program Development: Summer School |
131 \newblock In {\em Mathematical Methods in Program Development: Summer School |