[1] Amal Ahmed and David Walker. The logical approach to stack typing.
InACM SIGPLAN Workshop on Types in Language Design and Implementa-tion (TLDI 2003), pages 74–85, January 2003.
[2] Analog Devices. Digital Signal Processing Applications Using the ADSP-2100 Family. Prentice Hall, 1990.
[3] David Aspinall and Adriana B. Compagnoni. Heap bounded assembly language. Journal of Automated Reasoning, 2003. Special Issue on Proof-Carrying Code. To Appear.
[4] Randal E. Bryant. Graph-based algorithms for Boolean function manip-ulation. IEEE Transactions on Computers, C-35(8):677–691, 1986.
[5] Luca Cardelli. Type systems. In Allen B. Tucker, editor, Handbook of Computer Science and Engineering, chapter 103, pages 2208–2236. CRC Press, 1997.
[6] Luca Cardelli and Peter Wegner. On understanding types, data abstrac-tion, and polymorphism. Computing Surveys, 17(4):471–522, December 1985.
[7] William Chan, Richard Anderson, Paul Beame, and David Notkin. Com-bining constraint solving and symbolic model checking for a class of a systems with non-linear constraints. InComputer Aided Verification, pages 316–327, 1997.
[8] Juan Chen, Dinghao Wu, Andrew W. Appel, and Hai Fang. A provably sound TAL for back-end optimization. In PLDI 2003: ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 208–219, June 2003.
[9] James Cheney and Greg Morrisett. A linearly typed as-sembly language. Unpublished draft, available from http://www.cs.cornell.edu/people/jcheney, 2003.
[10] Wei-Ngan Chin, Siau-Cheng Khoo, and Dana N. Xu. Deriving pre-conditions for array bound check elimination. In Olivier Danvy and Andrzej Filinski, editors,Proceedings of Second Symposium on Programs as Data Objects (PADO-II), volume 2053 ofLecture Notes in Computer Science, pages 2–24. Springer-Verlag, 2001.
129
[11] James W. Cooley and John W. Tukey. An algorithm for the machine calculation of complex Fourier series. Mathematics of Computation, 19 (90):297–301, April 1965. ISSN 0025-5718.
[12] Karl Crary. Toward a foundational typed assembly language. In 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Lan-guages, pages 198–212, New Orleans, Louisiana, January 2003. ACM Press.
[13] Karl Crary and Stephanie Weirich. Resource bound certification. In Symposium on Principles of Programming Languages, pages 184–198, 2000.
[14] G. B. Dantzig and B. C. Eaves. Fourier-Motzkin elimination and its dual.
Journal of Combinatorial Theory (A), 14:288–297, 1973.
[15] DSP-C, 1998. DSP-C, release 9.9 edition, October 1998. An extension to ISO/IEC 9899:1990.
[16] Peter Harry Eidorff, Fritz Henglein, Christian Mossin, Henning Niss, Morten Heine Sørensen, and Mads Tofte. AnnoDomini: From type the-ory to year 2000 conversion tool. In26th ACM SIGPLAN-SIGACT Sym-posium on Principles of Programming Languages, pages 1–14, San Antonio, Texas, January 1999. ACM Press.
[17] Jean-Yves Girard. Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur. Thèse d’état, University of Paris VII, 1972.
Summary inProceedings of the Second Scandinavian Logic Symposium(J.E.
Fenstad, editor), North-Holland, 1971 (pp. 63–92).
[18] Kurt Gödel. Über formal unentscheidbare Sätze der Principia Math-ematica und verwandter System (On formal undecidable theorems in Principia Mathematica and related systems). InMonatshefte für Mathe-matik und Physik, volume 38, pages 173–198, 1931.
[19] Henrik Grauslund. Linear decision diagrams. Master’s thesis, Depart-ment of Information Technology, Technical University of Denmark, May 2000. Reference IT-E 843.
[20] Dan Grossman. Existential types for imperative languages. In Eleventh European Symposium on Programming, volume 2305 of Lecture Notes in Computer Science, pages 21–35, Grenoble, France, April 2002. Springer-Verlag.
[21] Dan Grossman and Greg Morrisett. Scalable certification for typed as-sembly language. Lecture Notes in Computer Science, 2071:117–145, 2001.
ISSN 0302-9743.
[22] Dan Grossman, Greg Morrisett, Trevor Jim, Michael Hicks, Yanling Wang, and James Cheney. Region-based memory management in Cy-clone. In ACM Conference on Programming Language Design and Imple-mentation, Berlin, Germany, June 2002. Extended version in Cornell CS Technical Report TR2001-1856.
[23] Robert Harper. A simplified account of polymorphic references. Infor-mation Processing Letters, 51:201–206, 1994.
[24] Charles Antony Richard Hoare. An axiomatic basis for computer pro-gramming. Communications of the ACM, 12(10):576–580, 1969.
[25] John Edward Hopcroft and Jeffrey David Ullman. Introduction to Au-tomata Theory, Languages, and Computation. Addison-Wesley, 1979.
[26] Samin Ishtiaq and Peter W. O’Hearn. BI as an assertion language for mutable data structures. InSymposium on Principles of Programming Lan-guages, pages 14–26, 2001.
[27] ISO/IEC 9899. Programming languages – C, 1990. ISO/IEC 9899:1990.
[28] Trevor Jim, Greg Morrisett, Dan Grossman, Michael Hicks, James Ch-eney, and Yanling Wang. Cyclone: A safe dialect of C. In USENIX Annual Technical Conference, Monterey, CA, June 2002.
[29] P. J. Landin. The mechanical evaluation of expressions.Computer journal, (6):308–320, 1964.
[30] Tim Lindholm and Frank Yellin. The Java Virtual Machine Specification.
Addison-Wesley, September 1996.
[31] Ian V. McLoughlin. DSP software development.
Linux Journal, (61), May 1999. Available from
http://linuxjournal.com/article.php?sid=3266.
[32] Jesper Blak Møller. Symbolic Model Checking of Real-Time Systems using Difference Decision Diagrams. PhD thesis, IT University of Copenhagen, April 2002.
[33] Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to typed assembly language. In 25th ACM SIGPLAN-SIGACT Sym-posium on Principles of Programming Languages, pages 85–97, San Diego, CA, USA, January 1998. ACM Press.
[34] Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, Daivd Walker, Stephanie Weirich, and Steve Zdancewic. TALx86: A realistic typed assembly language. InWorkshop on Compiler Support for System Software, pages 25–35, Atlanta, GA, USA, May 1999. INRIA Research Report 0228.
[35] Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From Sys-tem F to typed assembly language. ACM Transactions on Programming Languages and Systems, 21(3):528–569, May 1999.
[36] Greg Morrisett, Karl Crary, Neal Glew, and David Walker. Stack-based typed assembly language.Journal of Functional Programming, 12(1):43–88, January 2002.
[37] Michael Norrish. Kananaskis release of the theorem prover HOL4.
Homepage:http://www.hol.sf.net.
[38] Michael Norrish. Personal comunication, 2003.
[39] Peter W. O’Hearn and David J. Pym. The logic of bunched implications.
Bulletin of Symbolic Logic, 5(2):215–224, 1999.
[40] D. Oppen. A 222pn upper bound on the complexity of Presburger arith-metic. Journal of Computer and System Sciences, 16:323–332, 1978.
[41] Lars Pareto. Types for Crash Prevention. Phd. dissertation, Chalmers, Göteborg University, 2000.
[42] Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002.
[43] Mojzesz Presburger. Über die vollständigkeit eines gewissen systems der arithmetik ganzer zählen, in welchem die addition als einzige oper-ation hervortritt. Comptes-Rendus du I Congres de Mathematiciens des pays Slaves, pages 92–101, 1929.
[44] William Pugh. The Omega test: a fast and practical integer program-ming algorithm for dependence analysis.Communications of the ACM, 35 (8):102–114, August 1992.
[45] William Pugh and David Wonnacott. Experiences with constraint-based array dependence analysis. In Principles and Practice of Constraint Pro-gramming, pages 312–325, 1994.
[46] G. Ramalingam, John Field, and Frank Tip. Aggregate structure identi-fication and its application to program analysis. In26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 119–
132, San Antonio, Texas, January 1999. ACM Press.
[47] John C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proceedings of the Seventeenth Annual IEEE Symposium on Logic in Computer Science, Copenhagen, Denmark, July 2002.
[48] John C. Reynolds. Towards a theory of type structure. In Programming Symposium, volume 19 of Lecture Notes in Computer Science, pages 408–
425. Springer-Verlag, 1974.
[49] S. A. Seshia and R. E. Bryant. Unbounded, fully symbolic model checking of timed automata using boolean methods. In Jr. W. A. Hunt and F. Somenzi, editors, Computer-Aided Verifi-cation CAV 2003, volume 2725 of Lecture Notes in Computer Sci-ence, pages 154–166. Springer-Verlag, July 2003. Available as http://www.cs.cmu.edu/ bryant/pubdir/cav03c.ps.
[50] Frederick Smith, David Walker, and Greg Morrisett. Alias types. In Gert Smolka, editor,European Symposium on Programming, number 1782 in Lecture Notes in Computer Science, pages 366–381, March 2000.