Possibly infinite sequences in theorem provers: A comparative study

This publication has 13 references indexed in Scilit:

• Proof principles for datatypes with iterated recursion
  Published by Springer Nature ,1997
• Traces of I/O-automata in Isabelle/HOLCF
  Published by Springer Nature ,1997
• Computation on abstract data types. The extensional approach, with an application to streams
  Annals of Pure and Applied Logic, 1996
• Formal verification of a partial-order reduction technique for model checking
  Published by Springer Nature ,1996
• Formal verification for fault-tolerant architectures: prolegomena to the design of PVS
  IEEE Transactions on Software Engineering, 1995
• The temporal logic of actions
  ACM Transactions on Programming Languages and Systems, 1994
• Programming with streams in Coq a case study: The Sieve of Eratosthenes
  Published by Springer Nature ,1994
• Isabelle
  Published by Springer Nature ,1994
• Logic and Computation
  Published by Cambridge University Press (CUP) ,1987
• A formulation of the simple theory of types
  The Journal of Symbolic Logic, 1940