References

1

Stuart F. Allen, Robert L. Constable, Douglas J. Howe, and William Aitken.
The semantics of reflected proof.
In Proceedings of the Fifth Symposium on Logic in Computer Science, pages 95-197. IEEE, June 1990.

2

Lee Blaine and Allen Goldberg.
DTRE - A Semi-Automatic Transformation System.
In B. Möller, editor, Proceedings of the IFIP TC2 Working Conference on Constructing Programs from Specifications. ELSEVIER, 1991.

3

N. Bourbaki.
Elements of Mathematics, Algebra, Volume 1.
Addison-Wesley, Reading, MA, 1968.

4

James Caldwell.
Moving proofs-as-programs into practice.
In Proceedings of the Twelfth IEEE International Conference on Automated Software Engineering. IEEE Computer Society, 1997.

5

James Caldwell, Ian Gent, and Judith Underwood.
Search Algorithms in Type Theory.
Manuscript available at http://simon.cs.cornell.edu/Info/People/caldwell/index.html, September 1997.

6

Robert L. Constable et al.
Implementing Mathematics with the Nuprl Development System.
Prentice-Hall, NJ, 1986.

7

Cristina Cornes, Judicaël Courant, Jean-Christophe Filliâtre, Gérard Huet, Pascal Manoury, Christine Paulin-Mohring, César Muñoz, Chetan Murthy, Catherine Parent, Amokrane Saïbi, and Benjamin Werner.
The Coq Proof Assistant Reference Manual.
Technical report, INRIA, 1995.

8

G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, C. Paulin-Mohring, and B. Werner.
The Coq Proof Assistant User's Guide.
INRIA, Version 5.8, 1993.

9

Amy Felty and Frank Stomp.
A Correctness Proof of a Cache Coherence Protocol.
In Proceedings of the Eleventh Annual Conference on Computer Assurance, pages 128-141, 1996.

10

Amy P. Felty and Douglas J. Howe.
Hybrid Interactive Theorem Proving Using Nuprl and HOL.
In Fourteenth International Conference on Automated Deduction, volume 1249 of Lecture Notes in Computer Science, pages 351-365, Berlin, 1997. Springer-Verlag.

11

T. G. Griffin.
Notational Definition and Top-Down Refinement for Interactive Proof Development Systems.
PhD thesis, Cornell University, 1988.

12

Robert Harper, Furio Honsell, and Gordon Plotkin.
A Framework for Defining Logics.
Journal of the ACM, 40(1):143-184, 1992.
Preliminary version in LICS '87.

13

Gerard J. Holzmann.
Design and Validation of Computer Protocols.
Prentice-Hall Software Series, 1991.

14

Douglas J. Howe.
Equality in Lazy Computation Systems.
In Proceedings of Fourth Symposium on Logic in Computer Science, pages 198-203. IEEE Computer Society, June 1989.

15

Douglas J. Howe.
On Computational Open-Endedness in Martin-Löf's Type theory.
In Proceedings of Sixth Symposium on Logic in Computer Science, pages 162-172. IEEE Computer Society, 1991.

16

Douglas J. Howe.
Reasoning about Functional Programs in Nuprl.
Functional Programming, Concurrency, Simulation and Automated Reasoning, Vol. 693 of Lecture Notes in Computer Science, Springer, Berlin, 1993.

17

Douglas J. Howe.
Semantic Foundations for Embedding HOL in Nuprl.
In Martin Wirsing and Maurice Nivat, editors, Algebraic Methodology and Software Technology, volume 1101 of Lecture Notes in Computer Science, pages 85-101. Springer-Verlag, Berlin, 1996.

18

IEEE-P1596-05Nov90-doc197-iii.
Part IIIA: SCI Coherence Overview, 1990.
Unapproved Draft. Approved standard is described in IEEE Std. 1596-1992 ``The Scalable Coherent Interface''.

19

Christoph Kreitz.
Formal Mathematics for Verifiably Correct Program Synthesis.
Journal of the Interest Group in Pure and Applied Logics, 4(1):75-94, February 1996.

20

R. P. Kurshan.
Analysis of Discrete Event Coordination.
In Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness (REX Workshop), pages 414-453. Springer Verlag Lecture Notes in Computer Science 430, 1989.

21

Martin Löf.
Constructive Mathematics and Computer Programming.
In Proceedings of the Sixth International Congress for Logic, Methodology, and Philosophy of Science, pages 153-175, Amsterdam, 1982. North Holland.

22

K. L. McMillan.
Symbolic Model Checking.
Kluwer Academic Publishers, 1993.

23

P.F. Mendler.
Inductive Definition in Type Theory.
PhD thesis, Cornell University, Ithaca, NY, 1988.

24

B. Nordstrom, K. Petersson, and J. Smith.
Programming in Martin-Löf's Type Theory.
Oxford Sciences Publication, Oxford, 1990.

25

Sam Owre and Natarajan Shankar.
The Formal Semantics of PVS.
Technical report, SRI, August 1997.

26

Christine Paulin-Mohring.
Extracting F_w's Programs from Proofs in the Calculus of Constructions.
In Proceedings of the Sixteenth ACM Symposium on Principles of Programming Languages, pages 89-104, 1989.

27

Christine Paulin-Mohring and Benjamin Werner.
Synthesis of ML Programs in the System Coq.
Journal of Symbolic Computations, 15:607-640, 1993.

28

L. Paulson.
Logic and Computation: Interactive Proof with Cambridge LCF.
Cambridge University Press, NY, 1987.

29

L. Paulson and T. Nipkow.
Isabelle: A Generic Theorem Prover.
Vol. 825 of Lecture Notes in Computer Science, 1994.

30

D.R. Smith.
KIDS--A Knowledge-Based Software Development System.
In M.R. Lowry and R.D. McCartney, editors, Automating Software Design, pages 483-514. AAAI Press/MIT Press, Menlo Park, CA, 1991.

31

Y. V. Srinivas and Richard Jüllig.
Specware: Formal Support for Composing Software.
In Proceedings of the International Conference on the Mathematics of Program Construction, 1995.

32

Y. V. Srinivas and James L. McDonald.
The Architecture of SPECWARE, a Formal Software Development System.
Technical Report KES.U.96.7, KESTREL, 1996.

33

Ulrich Stern and David L. Dill.
Automatic Verification of the SCI Cache Coherence Protocol.
In Correct Hardware Design and Verification Methods: IFIP WG10.5 Advanced Research Working Conference Proceedings, 1995.

34

Carolyn Talcott.
A Theory for Program and Data Type Specification.
Theoretical Computer Science, 104(1):129-159, 1992.

35

Benjamin Werner.
Sets in Types, Types in Sets.
In International Symposium on Theoretical Aspects of Computer Software, Lecture Notes in Computer Science. Springer-Verlag, 1997.