Bibliography

1

H. Abelson and G. J. Sussman.
Structure and Interpretation of Computer Programs.
MIT Press, 1985.

2

H. B. Enderton.
A Mathematical Introduction to Logic.
Academic Press, 1972.

3

W. M. Farmer.
Abstract data types in many-sorted second-order logic.
Technical Report M87-64, The MITRE Corporation, 1987.

4

W. M. Farmer.
A partial functions version of Church's simple theory of types.
Journal of Symbolic Logic, 55:1269-91, 1990.

5

W. M. Farmer.
A simple type theory with partial functions and subtypes.
Annals of Pure and Applied Logic, 64:211-240, 1993.

6

W. M. Farmer.
A technique for safely extending axiomatic theories.
Technical report, The MITRE Corporation, 1993.

7

W. M. Farmer.
Theory interpretation in simple type theory.
In Proceedings, International Workshop on Higher Order Algebra, Logic and Term Rewriting (HOA '93), Amsterdam, The Netherlands, September 1993, Lecture Notes in Computer Science. Springer-Verlag, 1994.
Forthcoming.

8

W. M. Farmer, J. D. Guttman, M. E. Nadel, and F. J. Thayer.
Proof script pragmatics in IMPS.
In 12 International Conference on Automated Deduction (CADE-12), Lecture Notes in Computer Science. Springer-Verlag, 1994.
Forthcoming.

9

W. M. Farmer, J. D. Guttman, and F. J. Thayer.
IMPS: System description.
In D. Kapur, editor, Automated Deduction--CADE-11, volume 607 of Lecture Notes in Computer Science, pages 701-705. Springer-Verlag, 1992.

10

W. M. Farmer, J. D. Guttman, and F. J. Thayer.
Little theories.
In D. Kapur, editor, Automated Deduction--CADE-11, volume 607 of Lecture Notes in Computer Science, pages 567-581. Springer-Verlag, 1992.

11

W. M. Farmer, J. D. Guttman, and F. J. Thayer.
IMPS: an Interactive Mathematical Proof System.
Journal of Automated Reasoning, 11:213-248, 1993.

12

W. M. Farmer, J. D. Guttman, and F. J. Thayer.
Reasoning with contexts.
In A. Miola, editor, Design and Implementation of Symbolic Computation Systems, volume 722 of Lecture Notes in Computer Science, pages 216-228. Springer-Verlag, 1993.

13

W. M. Farmer and F. J. Thayer.
Two computer-supported proofs in metric space topology.
Notices of the American Mathematical Society, 38:1133-1138, 1991.

14

J. A. Goguen.
Principles of parameterized programming.
Technical report, SRI International, 1987.

15

J. A. Goguen and R. M. Burstall.
Introducing institutions.
In Logic of Programs, volume 164 of Lecture Notes in Computer Science, pages 221-256. Springer-Verlag, 1984.

16

J. D. Guttman.
A proposed interface logic for verification environments.
Technical Report M91-19, The MITRE Corporation, 1991.

17

J. D. Guttman.
Building verification environments from components: A position paper.
In Proceedings, Workshop on Effective Use of Automated Reasoning Technology in System Development, pages 4-17, Naval Research Laboratory, Washington, D.C., April 1992.

18

D. Kranz, R. Kelsey, J. Rees, P. Hudak, J. Philbin, and N. Adams.
ORBIT: An optimizing compiler for scheme.
In Proceedings of the SIGPLAN '86 Symposium on Compiler Construction, volume 21, pages 219-233, 1986.
Proceedings of the '86 Symposium on Compiler Construction.

19

J. D. Monk.
Mathematical Logic.
Springer-Verlag, 1976.

20

L. G. Monk.
Inference rules using local contexts.
Journal of Automated Reasoning, 4:445-462, 1988.

21

Y. N. Moschovakis.
Elementary Induction on Abstract Structures.
North-Holland, 1974.

22

Y. N. Moschovakis.
Abstract recursion as a foundation for the theory of algorithms.
In Computation and Proof Theory, Lecture Notes in Mathematics 1104, pages 289-364. Springer-Verlag, 1984.

23

J. A. Rees, N. I. Adams, and J. R. Meehan.
The T Manual.
Computer Science Department, Yale University, fifth edition, 1988.

24

J. R. Shoenfield.
Mathematical Logic.
Addison-Wesley, 1967.

25

R. M. Stallman.
GNU Emacs Manual (Version 18).
Free Software Foundation, sixth edition edition, 1987.

26

F. J. Thayer.
Obligated term replacements.
Technical Report MTR-10301, The MITRE Corporation, 1987.