Lecture Notes in Computer Science, Number 1125.
From Theorem Proving in Higher Order Logics: 9th International Conference. TPHOLs'97.
Edited by J. von Wright, J. Grundy, and J. Harrison.
Springer-Verlag, Turku, Finland.
August, 1996.
Pages 141–156.

This paper presents the formalisation of some elements of mathematical analysis using hte PVS verification system. our main motivation was to extend the existing PVS libraries and provide means of modelling and reasoning about hybrid systems. The paper focuses on several important aspects of PVS including recent extensions of the type system and discuesses their merits and effectiveness. We conclude by a brief comparison with similar developments using other theorem provers.

@InProceeding{dutertre96,
  AUTHOR = {Bruno Dutertre},
  TITLE = {Elements of Mathematical Analysis in {PVS}},
  NUMBER = {1125},
  YEAR = {1996},
  PAGES = {141--156},
  MONTH = {August},
  ADDRESS = {Turku, Finland},
  URL = {http://www.csl.sri.com/papers/tphol96/},
  SERIES = {Lecture Notes in Computer Science},
  BOOKTITLE = {Theorem Proving in Higher Order Logics: 9th International Conference. TPHOLs'97},
  PUBLISHER = {Springer-Verlag},
  EDITOR = {{J.} von Wright and {J.} Grundy and and {J.} Harrison}
}

• tphol96.ps.gz