References

1

BERSHAD, B., SAVAGE, S., PARDYAK, P., SIRER, E. G., BECKER, D., FIUCZYNSKI, M., CHAMBERS, C., AND EGGERS, S. Extensibility, safety and performance in the SPIN operating system. In Symposium on Operating System Principles (Dec. 1995), pp. 267-284.

2

BOYER, R. S., AND YU, Y. Automated proofs of object code for a widely used microprocessor. J. ACM 43, 1 (Jan. 1996), 166-192.

3

CLUTTERBUCK, D., AND CARR´E, B. The verification of low-level code. IEEE Software Engineering Journal 3, 3 (May 1988), 97-111.

4

CONSTABLE, R. L., ALLEN, S. F., BROMLEY, H. M., CLEAVELAND, W. R., CREMER, J. F., HARPER, R. W., HOWE, D. J., KNOBLOCK, T. B., MENDLER, N. P., PANANGADEN, P., SASAKI, J. T., AND SMITH, S. F. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986.

5

DIJKSTRA, E. W. Guarded commands, nondeterminancy and formal derivation of programs. Communications of the ACM 18 (1975), 453-457.

6

FLOYD, R. W. Assigning meanings to programs. In Mathematical Aspects of Computer Science, J. T. Schwartz, Ed. American Mathematical Society, 1967, pp. 19-32.

7

HARPER, R., HONSELL, F., AND PLOTKIN, G. A framework for defining logics. Journal of the Association for Computing Machinery 40, 1 (Jan. 1993), 143-184.

8

HOARE, C. A. R. An axiomatic basis for computer programming. Communications of the ACM 12 (1969), 567-580.

9

HSIEH, W. C., FIUCZYNSKI, M. E., GARRETT, C., SAVAGE, S., BECKER, D., AND BERSHAD, B. N. Language support for extensible operating systems. In The Inaugural Workshop on Compiler Support for Systems Software (Feb. 1996), pp. 127-133.

10

LEE, P., AND LEONE, M. Optimizing ML with run-time code generation. In PLDI'96 Conference on Programming Language Design and Implementation (May 1996), pp. 137-148.

11

MARTIN-LöF, P. A theory of types. Technical Report 71-3, Department of Mathematics, University of Stockholm, 1971.

12

MCCANNE, S. The Berkeley Packet Filter man page. BPF distribution available at ftp://ftp.ee.lbl.gov, May 1991.

13

MCCANNE, S., AND JACOBSON, V. The BSD packet filter: A new architecture for user-level packet capture. In The Winter 1993 USENIX Conference (Jan. 1993), USENIX Association, pp. 259-269.

14

MILNER, R., TOFTE, M., AND HARPER, R. The Definition of Standard ML. MIT Press, Cambridge, Massachusetts, 1990.

15

MOGUL, J. C., RASHID, R. F., AND ACCETTA, M. J. The packet filter: An efficient mechanism for user-level network code. In ACM Symposium on Operating Systems Principles (Nov. 1987), ACM Press, pp. 39-51. An updated version is available as DEC WRL Research Report 87/2.

16

NECULA, G. C., AND LEE, P. Proof-carrying code. Technical Report CMU-CS-96-165, Computer Science Department, Carnegie Mellon University, Sept. 1996. Also appeared as FOX memorandum CMU-CS-FOX-96-03.

17

NELSON, G. Systems Programming with MODULA-3. Prentice-Hall, 1991.

18

SIRER, E. G., SAVAGE, S., PARDYAK, P., DEFOUW, G. P., AND BERSHAD, B. N. Writing an operating system with Modula-3. In The Inaugural Workshop on Compiler Support for Systems Software (Feb. 1996), pp. 134-140.

19

SITES, R. L. Alpha Architecture Reference Manual. Digital Press, 1992.

20

SUN MICROSYSTEMS. The Java language specification. Available as
ftp://ftp.javasoft.com/docs/javaspec.ps.zip, 1995.

21

SUN MICROSYSTEMS. The Java Virtual Machine specification. Available as
ftp://ftp.javasoft.com/docs/vmspec.ps.zip, 1995.

22

TARDITI, D., MORRISETT, J. G., CHENG, P., STONE, C., HARPER, R., AND LEE, P. TIL: A type-directed optimizing compiler for ML. In PLDI'96 Conference on Programming Language Design and Implementation (May 1996), pp. 181-192.

23

WAHBE, R., LUCCO, S., ANDERSON, T. E., AND GRAHAM, S. L. Efficient software-based fault isolation. In 14th ACM Symposium on Operating Systems Principles (Dec. 1993), ACM, pp. 203-216.

24

WALLACH, D. A., ENGLER, D., AND KAASHOEK, M. F. ASHs : Application-specific handlers for high-performance messaging. In ACM SIGCOMM'96 (Oct. 1996), vol. 26, ACM.