Abstract
We compare four different formalizations of possibly infinite sequences in theorem provers based on higher-order logic. The formalizations have been carried out in different proof tools, namely in Gordon's HOL, in Isabelle and in PVS. The comparison considers different logics and proof infrastructures, but emphasizes on the proof principles that are available for each approach. The different formalizations discussed have been used not only to mechanize proofs of different properties of possibly infinite sequences, but also for the verification of some non-trivial theorems of concurrency theory.
Research supported by the Netherlands Organization for Scientific Research (NWO) under contract SION 612-316-125
Research supported by BMBF, KorSys
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Sten Agerholm. A HOL Basis for Reasoning about Functional Programs. PhD thesis, University of Aarhus, Denmark, 1994.
Alonzo Church. A formulation of the simple theory of types. J. Symbolic Logic, 5:56–68, 1940.
Ching-Tsun Chou and Doron Peled. Formal verification of a partial-order reduction technique for model checking. In T. Margaria and B. Steffen, editors, Proc. 2nd Workshop Tools and Algorithms for the Construction and Analysis of Systems (TACAS'96), volume 1055 of Lecture Notes in Computer Science. Springer-Verlag, 1996.
Marco Devillers and David Griffioen. A formalization of finite and infinite sequences in PVS. Technical Report CSI-89702, Computing Science Institute, University of Nijmegen, 1997.
Solomom Feferman. Computation on abstract data types. the extensional approach, with an application to streams. Annals of Pure and Applied Logic, 81:75–113, 1996.
M.C.J. Gordon and T.F. Melham. Introduction to HOL: a theorem-proving environment for higher-order logic. Cambridge University Press, 1993.
U. Hensel and B. Jacobs. Proof principles for datatypes with iterated recursion. Technical Report CSI-89703, Computing Science Institute, University of Nijmegen, 1997.
Leslie Lamport. The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems, 16(3):872–923, May 1994.
Francois Leclerc and Christine Paulin-Mohring. Programming with streams in Coq, a case study: the sieve of eratosthenes. In H. Barendregt and T. Nipkow, editors, Proc. Types for Proofs and Programs (TYPES'93), volume 806 of Lecture Notes in Computer Science, 1993.
Nancy Lynch and Mark Tuttle. An introduction to Input/Output automata. CWI Quarterly, 2(3):219–246, 1989.
Olaf Müller and Tobias Nipkow. Traces of I/O-Automata in Isabelle/HOLCF. In Proc. 7th Int. Joint Conf. on Theory and Practice of Software Development (TAPSOFT'97), Lecture Notes in Computer Science. Springer-Verlag, 1997.
Olaf Müller and Konrad Slind. Isabelle/HOL as a platform for partiality. In CADE-13 Workshop: Mechanization of Partial Functions, New Brunswick, pages 85–96, 1996.
Tobias Nipkow and Konrad Slind. 1/O automata in Isabelle/HOL. In P. Dybjer, B. Nordström, and J. Smith, editors, Types for Proofs and Programs, volume 996 of Lecture Notes in Computer Science, pages 101–119. Springer-Verlag, 1995.
S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107–125, February 1995.
Lawrence C. Paulson. Logic and Computation. Cambridge University Press, 1987.
Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.
Lawrence C. Paulson. Mechanizing coinduction and corecursion in higher-order logic. J. Automated Reasoning, 7, 1997.
Franz Regensburger. HOLCF: Higher Order Logic of Computable Functions. In E.T. Schubert, P.J. Windley, and J. Alves-Foss, editors, Higher Order Logic Theorem Proving and its Applications, volume 971 of Lecture Notes in Computer Science, pages 293–307. Springer-Verlag, 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Devillers, M., Griffioen, D., Müller, O. (1997). Possibly infinite sequences in theorem provers: A comparative study. In: Gunter, E.L., Felty, A. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1997. Lecture Notes in Computer Science, vol 1275. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028388
Download citation
DOI: https://doi.org/10.1007/BFb0028388
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63379-2
Online ISBN: 978-3-540-69526-4
eBook Packages: Springer Book Archive